1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Oct 05 10:30:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Oct 05 10:59:12 2010 +0200
     1.3 @@ -16,7 +16,8 @@
     1.4    val finish_cnf: thm list -> thm list
     1.5    val presimplify: thm -> thm
     1.6    val make_nnf: Proof.context -> thm -> thm
     1.7 -  val skolemize_with_choice_thms : Proof.context -> thm list -> thm -> thm
     1.8 +  val choice_theorems : theory -> thm list
     1.9 +  val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
    1.10    val skolemize : Proof.context -> thm -> thm
    1.11    val is_fol_term: theory -> term -> bool
    1.12    val make_clauses_unsorted: thm list -> thm list
    1.13 @@ -554,9 +555,12 @@
    1.14      [] => th |> presimplify |> make_nnf1 ctxt
    1.15    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    1.16  
    1.17 +fun choice_theorems thy =
    1.18 +  try (Global_Theory.get_thm thy) "Hilbert_Choice.choice" |> the_list
    1.19 +
    1.20  (* Pull existential quantifiers to front. This accomplishes Skolemization for
    1.21     clauses that arise from a subgoal. *)
    1.22 -fun skolemize_with_choice_thms ctxt choice_ths =
    1.23 +fun skolemize_with_choice_theorems ctxt choice_ths =
    1.24    let
    1.25      fun aux th =
    1.26        if not (has_conns [@{const_name Ex}] (prop_of th)) then
    1.27 @@ -574,7 +578,10 @@
    1.28                        |> forward_res ctxt aux
    1.29    in aux o make_nnf ctxt end
    1.30  
    1.31 -fun skolemize ctxt = skolemize_with_choice_thms ctxt (Meson_Choices.get ctxt)
    1.32 +fun skolemize ctxt =
    1.33 +  let val thy = ProofContext.theory_of ctxt in
    1.34 +    skolemize_with_choice_theorems ctxt (choice_theorems thy)
    1.35 +  end
    1.36  
    1.37  (* "RS" can fail if "unify_search_bound" is too small. *)
    1.38  fun try_skolemize ctxt th =