--- 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 =