src/ZF/Tools/induct_tacs.ML
changeset 44058 ae85c5d64913
parent 42361 23f352990944
child 46947 b8c7eb0c2f89
--- a/src/ZF/Tools/induct_tacs.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -123,8 +123,7 @@
                               Syntax.string_of_term_global thy eqn);
 
     val constructors =
-        map (head_of o const_of o FOLogic.dest_Trueprop o
-             #prop o rep_thm) case_eqns;
+        map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
 
     val Const (@{const_name mem}, _) $ _ $ data =
         FOLogic.dest_Trueprop (hd (prems_of elim));