# HG changeset patch
# User blanchet
# Date 1285581653 -7200
# Node ID 76a61ca09d5d890f3d024c2f8eda63aaf7d583f4
# Parent  0b93a954da4f9b8473e9652ebf1e312964c1e3f5
renamed function

diff -r 0b93a954da4f -r 76a61ca09d5d src/HOL/Tools/Sledgehammer/meson_clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/meson_clausifier.ML	Mon Sep 27 10:44:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausifier.ML	Mon Sep 27 12:00:53 2010 +0200
@@ -11,7 +11,7 @@
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm
   val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
-  val cnf_axiom : theory -> thm -> thm list
+  val meson_cnf_axiom : theory -> thm -> thm list
   val meson_general_tac : Proof.context -> thm list -> int -> tactic
   val setup: theory -> theory
 end;
@@ -234,7 +234,7 @@
   in Thm.equal_elim eqth th end
 
 (* Convert a theorem to CNF, with Skolem functions as additional premises. *)
-fun cnf_axiom thy th =
+fun meson_cnf_axiom thy th =
   let
     val ctxt0 = Variable.global_thm_context th
     val (nnf_th, ctxt) = to_nnf th ctxt0
@@ -257,7 +257,7 @@
   let
     val thy = ProofContext.theory_of ctxt
     val ctxt0 = Classical.put_claset HOL_cs ctxt
-  in Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) end
+  in Meson.meson_tac ctxt0 (maps (meson_cnf_axiom thy) ths) end
 
 val setup =
   Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
diff -r 0b93a954da4f -r 76a61ca09d5d src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 27 10:44:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 27 12:00:53 2010 +0200
@@ -57,7 +57,7 @@
       val type_lits = Config.get ctxt type_lits
       val th_cls_pairs =
         map (fn th => (Thm.get_name_hint th,
-                       Meson_Clausifier.cnf_axiom thy th)) ths0
+                       Meson_Clausifier.meson_cnf_axiom thy th)) ths0
       val ths = maps #2 th_cls_pairs
       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls