src/ZF/Tools/datatype_package.ML

--- 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);