src/HOL/Tools/Meson/meson_clausify.ML
changeset 40262 8403085384eb
parent 40261 7a02144874f3
child 40263 51ed7a5ad4c5
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 29 12:49:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 29 12:49:05 2010 +0200
     1.3 @@ -346,13 +346,13 @@
     1.4                |>> the_single |>> cterm_of thy
     1.5            in
     1.6              (SOME (discharger_th, fully_skolemized_ct),
     1.7 -                   Thm.assume fully_skolemized_ct, ctxt)
     1.8 +             (Thm.assume fully_skolemized_ct, ctxt))
     1.9            end
    1.10         else
    1.11 -         (NONE, th, ctxt)
    1.12 +         (NONE, (th, ctxt))
    1.13        end
    1.14      else
    1.15 -      (NONE, th, ctxt)
    1.16 +      (NONE, (th, ctxt))
    1.17    end
    1.18  
    1.19  (* Convert a theorem to CNF, with additional premises due to skolemization. *)
    1.20 @@ -360,7 +360,8 @@
    1.21    let
    1.22      val thy = ProofContext.theory_of ctxt0
    1.23      val choice_ths = choice_theorems thy
    1.24 -    val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
    1.25 +    val (opt, (nnf_th, ctxt)) =
    1.26 +      nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
    1.27      fun clausify th =
    1.28        make_cnf (if new_skolemizer orelse null choice_ths then
    1.29                    []
    1.30 @@ -370,6 +371,7 @@
    1.31      val (cnf_ths, ctxt) =
    1.32        clausify nnf_th
    1.33        |> (fn ([], _) =>
    1.34 +             (* FIXME: This probably doesn't work with the new Skolemizer *)
    1.35               clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
    1.36             | p => p)
    1.37      fun intr_imp ct th =