src/HOL/Tools/Metis/metis_tactics.ML
changeset 42739 017e5dac8642
parent 42733 01ef1c3d9cfd
child 42747 f132d13fcf75
     1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -141,10 +141,11 @@
     1.4      else th :: Meson.make_clauses_unsorted [th']
     1.5    end
     1.6  
     1.7 -val neg_clausify =
     1.8 +fun neg_clausify ctxt =
     1.9    single
    1.10    #> Meson.make_clauses_unsorted
    1.11 -  #> maps also_extensionalize_theorem
    1.12 +  #> maps (Raw_Simplifier.rewrite_rule (Meson.unfold_set_const_simps ctxt)
    1.13 +           #> also_extensionalize_theorem)
    1.14    #> map Meson_Clausify.introduce_combinators_in_theorem
    1.15    #> Meson.finish_cnf
    1.16  
    1.17 @@ -168,7 +169,7 @@
    1.18        (verbose_warning ctxt "Proof state contains the universal sort {}";
    1.19         Seq.empty)
    1.20      else
    1.21 -      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
    1.22 +      Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt))
    1.23                    (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
    1.24                    ctxt i st0
    1.25    end