src/HOL/Tools/res_axioms.ML
changeset 35625 9c818cab0dd0
parent 35624 c4e29a0bb8c1
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -276,7 +276,7 @@
     1.4    let val th1 = th |> transform_elim |> zero_var_indexes
     1.5        val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
     1.6        val th3 = th2
     1.7 -        |> Conv.fconv_rule ObjectLogic.atomize
     1.8 +        |> Conv.fconv_rule Object_Logic.atomize
     1.9          |> Meson.make_nnf ctxt |> strip_lambdas ~1
    1.10    in  (th3, ctxt)  end;
    1.11  
    1.12 @@ -493,7 +493,7 @@
    1.13  (*** Converting a subgoal into negated conjecture clauses. ***)
    1.14  
    1.15  fun neg_skolemize_tac ctxt =
    1.16 -  EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac ctxt];
    1.17 +  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
    1.18  
    1.19  val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
    1.20