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