The following code works: datatype 'a bintree = Branch "'a bintree" "'a bintree" | Tip 'a definition "test1 = (Tip True = Branch (Tip False) (Tip True))" export_code test1 in Haskell file -
but this other example doesn't: datatype 'a tree = Node 'a "'a tree list" definition "test2 = (Node True [] = Node True [Node False []])" export_code test2 in Haskell file - Instead it fails with: *** exception UNDEF raised *** At command "export_code". I figured that someone must have known about this already; what tipped me off to the existence of this bug was the custom [code] rule for eq_class.eq given in the Typerep theory. (The log file says something about dropping the previously-installed code equations.) I'm just wondering if there is a solution in the works. Honestly, the primary reason I'm interested is that I'd like to see Typerep.thy moved into Plain, and currently the eq_class.eq [code] rule adds a dependency on the list_all2 function, which I'd like to get rid of. - Brian
