restructure Skolemization code slightly
authorblanchet
Fri Oct 29 12:49:05 2010 +0200 (2010-10-29)
changeset 4026351ed7a5ad4c5
parent 40262 8403085384eb
child 40264 b91e2e16d994
restructure Skolemization code slightly
src/HOL/Tools/Meson/meson_clausify.ML
     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 @@ -328,14 +328,13 @@
     1.4          val discharger_th =
     1.5            th |> (if no_choice then pull_out else skolemize choice_ths)
     1.6          val fully_skolemized_t =
     1.7 -          th |> prop_of
     1.8 -             |> no_choice ? rename_bound_vars_to_be_zapped ax_no
     1.9 -             |> Skip_Proof.make_thm thy |> skolemize [cheat_choice] |> cprop_of
    1.10 -             |> not no_choice
    1.11 -                ? (term_of #> rename_bound_vars_to_be_zapped ax_no
    1.12 -                   #> cterm_of thy)
    1.13 -             |> zap true |> Drule.export_without_context
    1.14 -             |> cprop_of |> Thm.dest_equals |> snd |> term_of
    1.15 +          discharger_th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
    1.16 +          |> (if no_choice then
    1.17 +                Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> cprop_of
    1.18 +              else
    1.19 +                cterm_of thy)
    1.20 +          |> zap true |> Drule.export_without_context
    1.21 +          |> cprop_of |> Thm.dest_equals |> snd |> term_of
    1.22        in
    1.23          if exists_subterm (fn Var ((s, _), _) =>
    1.24                                String.isPrefix new_skolem_var_prefix s