# HG changeset patch
# User blanchet
# Date 1280243712 -7200
# Node ID 135f7d48949259b4f964074efec4ed634c1bc950
# Parent  b30c3c2e1030a9e464a8eb4db4fdeda2897c0129
get rid of more dead wood

diff -r b30c3c2e1030 -r 135f7d489492 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jul 27 17:04:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jul 27 17:15:12 2010 +0200
@@ -8,9 +8,7 @@
 signature CLAUSIFIER =
 sig
   val introduce_combinators_in_cterm : cterm -> thm
-  val cnf_axiom: theory -> bool -> thm -> thm list
-  val cnf_rules_pairs :
-    theory -> bool -> (string * thm) list -> ((string * int) * thm) list
+  val cnf_axiom: theory -> thm -> thm list
   val neg_clausify: thm -> thm list
 end;
 
@@ -198,7 +196,7 @@
 (* Given the definition of a Skolem function, return a theorem to replace
    an existential formula by a use of that function.
    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
-fun skolem_theorem_of_def thy cheat rhs0 =
+fun skolem_theorem_of_def thy rhs0 =
   let
     val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy
     val rhs' = rhs |> Thm.dest_comb |> snd
@@ -214,12 +212,8 @@
       Drule.list_comb (rhs, frees)
       |> Drule.beta_conv cabs |> Thm.capply cTrueprop
     fun tacf [prem] =
-      if cheat then
-        Skip_Proof.cheat_tac thy
-      else
-        rewrite_goals_tac skolem_id_def_raw
-        THEN rtac ((prem |> rewrite_rule skolem_id_def_raw)
-                   RS @{thm someI_ex}) 1
+      rewrite_goals_tac skolem_id_def_raw
+      THEN rtac ((prem |> rewrite_rule skolem_id_def_raw) RS @{thm someI_ex}) 1
   in
     Goal.prove_internal [ex_tm] conc tacf
     |> forall_intr_list frees
@@ -238,11 +232,11 @@
   in  (th3, ctxt)  end;
 
 (* Skolemize a named theorem, with Skolem functions as additional premises. *)
-fun skolemize_theorem thy cheat th =
+fun skolemize_theorem thy th =
   let
     val ctxt0 = Variable.global_thm_context th
     val (nnfth, ctxt) = to_nnf th ctxt0
-    val sko_ths = map (skolem_theorem_of_def thy cheat)
+    val sko_ths = map (skolem_theorem_of_def thy)
                       (assume_skolem_funs nnfth)
     val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
   in
@@ -255,25 +249,7 @@
 
 (* Convert Isabelle theorems into axiom clauses. *)
 (* FIXME: is transfer necessary? *)
-fun cnf_axiom thy cheat = skolemize_theorem thy cheat o Thm.transfer thy
-
-
-(**** Translate a set of theorems into CNF ****)
-
-(*The combination of rev and tail recursion preserves the original order*)
-(* ### FIXME: kill "cheat" *)
-fun cnf_rules_pairs thy cheat =
-  let
-    fun do_one _ [] = []
-      | do_one ((name, k), th) (cls :: clss) =
-        ((name, k), cls) :: do_one ((name, k + 1), th) clss
-    fun do_all pairs [] = pairs
-      | do_all pairs ((name, th) :: ths) =
-        let
-          val new_pairs = do_one ((name, 0), th) (cnf_axiom thy cheat th)
-                          handle THM _ => []
-        in do_all (new_pairs @ pairs) ths end
-  in do_all [] o rev end
+fun cnf_axiom thy = skolemize_theorem thy o Thm.transfer thy
 
 
 (*** Converting a subgoal into negated conjecture clauses. ***)
diff -r b30c3c2e1030 -r 135f7d489492 src/HOL/Tools/Sledgehammer/meson_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Tue Jul 27 17:04:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Tue Jul 27 17:15:12 2010 +0200
@@ -18,7 +18,7 @@
   let
     val thy = ProofContext.theory_of ctxt
     val ctxt0 = Classical.put_claset HOL_cs ctxt
-  in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy false) ths) end
+  in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end
 
 val setup =
   Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
diff -r b30c3c2e1030 -r 135f7d489492 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jul 27 17:04:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jul 27 17:15:12 2010 +0200
@@ -599,7 +599,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun cnf_helper_theorem thy raw th =
-  if raw then th else the_single (Clausifier.cnf_axiom thy false th)
+  if raw then th else the_single (Clausifier.cnf_axiom thy th)
 
 fun type_ext thy tms =
   let val subs = tfree_classes_of_terms tms
@@ -715,7 +715,7 @@
 fun FOL_SOLVE mode ctxt cls ths0 =
   let val thy = ProofContext.theory_of ctxt
       val th_cls_pairs =
-        map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy false th)) ths0
+        map (fn th => (Thm.get_name_hint th, Clausifier.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