1.1 --- a/src/ZF/Tools/datatype_package.ML	Mon Aug 08 16:38:59 2011 +0200
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon Aug 08 17:23:15 2011 +0200
     1.3 @@ -339,7 +339,7 @@
     1.4        end
     1.5  
     1.6    val constructors =
     1.7 -      map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
     1.8 +      map (head_of o #1 o Logic.dest_equals o Thm.prop_of) (tl con_defs);
     1.9  
    1.10    val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs);
    1.11