src/HOL/Tools/Sledgehammer/metis_tactics.ML
changeset 39720 0b93a954da4f
parent 39594 624d6c0e220d
child 39721 76a61ca09d5d
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 27 09:17:24 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 27 10:44:08 2010 +0200
     1.3 @@ -56,7 +56,8 @@
     1.4    let val thy = ProofContext.theory_of ctxt
     1.5        val type_lits = Config.get ctxt type_lits
     1.6        val th_cls_pairs =
     1.7 -        map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0
     1.8 +        map (fn th => (Thm.get_name_hint th,
     1.9 +                       Meson_Clausifier.cnf_axiom thy th)) ths0
    1.10        val ths = maps #2 th_cls_pairs
    1.11        val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
    1.12        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
    1.13 @@ -116,7 +117,7 @@
    1.14     does, but also keep an unextensionalized version of "th" for backward
    1.15     compatibility. *)
    1.16  fun also_extensionalize_theorem th =
    1.17 -  let val th' = Clausifier.extensionalize_theorem th in
    1.18 +  let val th' = Meson_Clausifier.extensionalize_theorem th in
    1.19      if Thm.eq_thm (th, th') then [th]
    1.20      else th :: Meson.make_clauses_unsorted [th']
    1.21    end
    1.22 @@ -125,7 +126,7 @@
    1.23    single
    1.24    #> Meson.make_clauses_unsorted
    1.25    #> maps also_extensionalize_theorem
    1.26 -  #> map Clausifier.introduce_combinators_in_theorem
    1.27 +  #> map Meson_Clausifier.introduce_combinators_in_theorem
    1.28    #> Meson.finish_cnf
    1.29  
    1.30  fun preskolem_tac ctxt st0 =