src/HOL/Library/Efficient_Nat.thy
changeset 35625 9c818cab0dd0
parent 34944 970e1466028d
child 35689 c3bef0c972d7
--- a/src/HOL/Library/Efficient_Nat.thy	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Sun Mar 07 12:19:47 2010 +0100
@@ -181,7 +181,7 @@
       | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
       | find_var _ = NONE;
     fun find_thm th =
-      let val th' = Conv.fconv_rule ObjectLogic.atomize th
+      let val th' = Conv.fconv_rule Object_Logic.atomize th
       in Option.map (pair (th, th')) (find_var (prop_of th')) end
   in
     case get_first find_thm thms of
@@ -189,7 +189,7 @@
     | SOME ((th, th'), (Sucv, v)) =>
         let
           val cert = cterm_of (Thm.theory_of_thm th);
-          val th'' = ObjectLogic.rulify (Thm.implies_elim
+          val th'' = Object_Logic.rulify (Thm.implies_elim
             (Conv.fconv_rule (Thm.beta_conversion true)
               (Drule.instantiate' []
                 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,