changeset 35625 | 9c818cab0dd0 |
parent 33957 | e9afca2118d4 |
child 36960 | 01594f816e3a |
--- a/src/Tools/induct_tacs.ML Sun Mar 07 11:57:16 2010 +0100 +++ b/src/Tools/induct_tacs.ML Sun Mar 07 12:19:47 2010 +0100 @@ -92,7 +92,7 @@ (_, rule) :: _ => rule | [] => raise THM ("No induction rules", 0, []))); - val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize); + val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize); val _ = Method.trace ctxt [rule']; val concls = Logic.dest_conjunctions (Thm.concl_of rule);