| changeset 32461 | eee4fa79398f |
| parent 28562 | 4e74209f113e |
| child 33954 | 1bc3b688548c |
--- a/src/HOL/MicroJava/J/TypeRel.thy Mon Aug 31 17:32:29 2009 +0200 +++ b/src/HOL/MicroJava/J/TypeRel.thy Mon Aug 31 20:32:00 2009 +0200 @@ -97,6 +97,14 @@ qed qed +text {* Code generator setup (FIXME!) *} + +consts_code + "wfrec" ("\<module>wfrec?") +attach {* +fun wfrec f x = f (wfrec f) x; +*} + consts method :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)