--- a/src/HOL/Tools/Meson/meson.ML Tue Oct 05 10:30:50 2010 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Tue Oct 05 10:59:12 2010 +0200
@@ -16,7 +16,8 @@
val finish_cnf: thm list -> thm list
val presimplify: thm -> thm
val make_nnf: Proof.context -> thm -> thm
- val skolemize_with_choice_thms : Proof.context -> thm list -> thm -> thm
+ val choice_theorems : theory -> thm list
+ val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
val skolemize : Proof.context -> thm -> thm
val is_fol_term: theory -> term -> bool
val make_clauses_unsorted: thm list -> thm list
@@ -554,9 +555,12 @@
[] => th |> presimplify |> make_nnf1 ctxt
| _ => raise THM ("make_nnf: premises in argument", 0, [th]);
+fun choice_theorems thy =
+ try (Global_Theory.get_thm thy) "Hilbert_Choice.choice" |> the_list
+
(* Pull existential quantifiers to front. This accomplishes Skolemization for
clauses that arise from a subgoal. *)
-fun skolemize_with_choice_thms ctxt choice_ths =
+fun skolemize_with_choice_theorems ctxt choice_ths =
let
fun aux th =
if not (has_conns [@{const_name Ex}] (prop_of th)) then
@@ -574,7 +578,10 @@
|> forward_res ctxt aux
in aux o make_nnf ctxt end
-fun skolemize ctxt = skolemize_with_choice_thms ctxt (Meson_Choices.get ctxt)
+fun skolemize ctxt =
+ let val thy = ProofContext.theory_of ctxt in
+ skolemize_with_choice_theorems ctxt (choice_theorems thy)
+ end
(* "RS" can fail if "unify_search_bound" is too small. *)
fun try_skolemize ctxt th =