src/HOL/Tools/Metis/metis_tactics.ML
changeset 42747 f132d13fcf75
parent 42739 017e5dac8642
child 42847 06d3ce527d29
     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 @@ -132,20 +132,9 @@
     1.4                    (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
     1.5                     else ""))
     1.6  
     1.7 -(* Extensionalize "th", because that makes sense and that's what Sledgehammer
     1.8 -   does, but also keep an unextensionalized version of "th" for backward
     1.9 -   compatibility. *)
    1.10 -fun also_extensionalize_theorem th =
    1.11 -  let val th' = Meson_Clausify.extensionalize_theorem th in
    1.12 -    if Thm.eq_thm (th, th') then [th]
    1.13 -    else th :: Meson.make_clauses_unsorted [th']
    1.14 -  end
    1.15 -
    1.16  fun neg_clausify ctxt =
    1.17    single
    1.18    #> Meson.make_clauses_unsorted
    1.19 -  #> maps (Raw_Simplifier.rewrite_rule (Meson.unfold_set_const_simps ctxt)
    1.20 -           #> also_extensionalize_theorem)
    1.21    #> map Meson_Clausify.introduce_combinators_in_theorem
    1.22    #> Meson.finish_cnf
    1.23