changeset 44058 | ae85c5d64913 |
parent 42793 | 88bee9f6eec7 |
child 44241 | 7943b69f0188 |
--- a/src/ZF/Tools/datatype_package.ML Mon Aug 08 16:38:59 2011 +0200 +++ b/src/ZF/Tools/datatype_package.ML Mon Aug 08 17:23:15 2011 +0200 @@ -339,7 +339,7 @@ end val constructors = - map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs); + map (head_of o #1 o Logic.dest_equals o Thm.prop_of) (tl con_defs); val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs);