# HG changeset patch
# User blanchet
# Date 1288349345 -7200
# Node ID 51ed7a5ad4c5b5ddab9549c8039abdde6ac7cc6c
# Parent  8403085384eb9a04fa217ef4a7c41ec4dd15aa72
restructure Skolemization code slightly

diff -r 8403085384eb -r 51ed7a5ad4c5 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 29 12:49:05 2010 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 29 12:49:05 2010 +0200
@@ -328,14 +328,13 @@
         val discharger_th =
           th |> (if no_choice then pull_out else skolemize choice_ths)
         val fully_skolemized_t =
-          th |> prop_of
-             |> no_choice ? rename_bound_vars_to_be_zapped ax_no
-             |> Skip_Proof.make_thm thy |> skolemize [cheat_choice] |> cprop_of
-             |> not no_choice
-                ? (term_of #> rename_bound_vars_to_be_zapped ax_no
-                   #> cterm_of thy)
-             |> zap true |> Drule.export_without_context
-             |> cprop_of |> Thm.dest_equals |> snd |> term_of
+          discharger_th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
+          |> (if no_choice then
+                Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> cprop_of
+              else
+                cterm_of thy)
+          |> zap true |> Drule.export_without_context
+          |> cprop_of |> Thm.dest_equals |> snd |> term_of
       in
         if exists_subterm (fn Var ((s, _), _) =>
                               String.isPrefix new_skolem_var_prefix s