Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/res_axioms.ML
changeset 35625 9c818cab0dd0
parent 35624 c4e29a0bb8c1 
--- a/src/HOL/Tools/res_axioms.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -276,7 +276,7 @@
   let val th1 = th |> transform_elim |> zero_var_indexes
       val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
       val th3 = th2
-        |> Conv.fconv_rule ObjectLogic.atomize
+        |> Conv.fconv_rule Object_Logic.atomize
         |> Meson.make_nnf ctxt |> strip_lambdas ~1
   in  (th3, ctxt)  end;
 
@@ -493,7 +493,7 @@
 (*** Converting a subgoal into negated conjecture clauses. ***)
 
 fun neg_skolemize_tac ctxt =
-  EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac ctxt];
+  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
 
 val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
isabelle