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