author blanchet Tue, 01 Jul 2014 16:47:10 +0200 changeset 57466 feb414dadfd1 parent 57465 ed826e2053c9 child 57467 03345dad8430
```--- 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 =```