# HG changeset patch
# User blanchet
# Date 1404226030 -7200
# Node ID feb414dadfd15ffae03c820c931a3f1aed3dbf6a
# Parent  ed826e2053c99db43c83bb0600c7ec9fb0beb608
use context instead of theory

diff -r ed826e2053c9 -r feb414dadfd1 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Jul 01 16:47:10 2014 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Jul 01 16:47:10 2014 +0200
@@ -190,10 +190,9 @@
 (* Given the definition of a Skolem function, return a theorem to replace
    an existential formula by a use of that function.
    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
-fun old_skolem_theorem_of_def thy rhs0 =
+fun old_skolem_theorem_of_def ctxt rhs0 =
   let
-    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
-
+    val thy = Proof_Context.theory_of ctxt
     val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
     val rhs' = rhs |> Thm.dest_comb |> snd
     val (ch, frees) = c_variant_abs_multi (rhs', [])
@@ -201,8 +200,7 @@
     val T =
       case hilbert of
         Const (_, Type (@{type_name fun}, [_, T])) => T
-      | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"",
-                         [hilbert])
+      | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert])
     val cex = cterm_of thy (HOLogic.exists_const T)
     val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
     val conc =
@@ -373,7 +371,7 @@
       nnf_axiom choice_ths new_skolem ax_no th ctxt0
     fun clausify th =
       make_cnf (if new_skolem orelse null choice_ths then []
-                else map (old_skolem_theorem_of_def thy) (old_skolem_defs th))
+                else map (old_skolem_theorem_of_def ctxt) (old_skolem_defs th))
                th ctxt ctxt
     val (cnf_ths, ctxt) = clausify nnf_th
     fun intr_imp ct th =