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