[isabelle-dev] "rep_datatype" is illegal in local theory mode

[Christian Sternagel]

Hi all,

I am just curious whether the reason for rep_datatype being illegal in 
local theory mode is that the datatype package is not fully localized 
yet (in which case it is conceivable that this will work some day, which 
would be nice) or that this is inherently not possible to realize?

cheers

chris

PS: I am just playing around with a locale for finite trees and wanted 
to introduce some recursive functions (and later also inductive 
predicates) but pattern matching is only possible on constructors. Is 
anybody aware of an earlier attempt for doing such a thing or a better 
way to prove something "for all kinds of (non empty) finite trees"?