src/Tools/induct.ML
changeset 35625 9c818cab0dd0
parent 35624 c4e29a0bb8c1
child 36602 0cbcdfd9e527
     1.1 --- a/src/Tools/induct.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/Tools/induct.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -137,7 +137,7 @@
     1.4        Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv
     1.5        Conv.rewr_conv Drule.swap_prems_eq
     1.6  
     1.7 -fun drop_judgment ctxt = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt);
     1.8 +fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt);
     1.9  
    1.10  fun find_eq ctxt t =
    1.11    let
    1.12 @@ -511,7 +511,7 @@
    1.13  
    1.14  fun atomize_term thy =
    1.15    MetaSimplifier.rewrite_term thy Data.atomize []
    1.16 -  #> ObjectLogic.drop_judgment thy;
    1.17 +  #> Object_Logic.drop_judgment thy;
    1.18  
    1.19  val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
    1.20