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