# HG changeset patch
# User paulson
# Date 1192021542 -7200
# Node ID 5f5679e2ec2f7be7d78add80a58a11406558d619
# Parent  39a23aadc7e124a8960cbfeebb267cb58fa2d1c3
removed dead code

diff -r 39a23aadc7e1 -r 5f5679e2ec2f src/HOL/ATP_Linkup.thy
--- a/src/HOL/ATP_Linkup.thy	Wed Oct 10 15:05:34 2007 +0200
+++ b/src/HOL/ATP_Linkup.thy	Wed Oct 10 15:05:42 2007 +0200
@@ -38,15 +38,6 @@
 definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
   where "COMBS P Q R == P R (Q R)"
 
-definition COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c"
-  where "COMBB' M P Q R == M (P (Q R))"
-
-definition COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c"
-  where "COMBC' M P Q R == M (P R) Q"
-
-definition COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c"
-  where "COMBS' M P Q R == M (P R) (Q R)"
-
 definition fequal :: "'a => 'a => bool"
   where "fequal X Y == (X=Y)"
 
diff -r 39a23aadc7e1 -r 5f5679e2ec2f src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Wed Oct 10 15:05:34 2007 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Wed Oct 10 15:05:42 2007 +0200
@@ -2,10 +2,6 @@
    Author: Jia Meng, NICTA
 
 FOL clauses translated from HOL formulae.
-
-The combinator code needs to be deleted after the translation paper has been published.
-It cannot be used with proof reconstruction because combinators are not introduced by proof.
-The Turner combinators (B', C', S') yield no improvement and should be deleted.
 *)
 
 signature RES_HOL_CLAUSE =
@@ -49,9 +45,6 @@
 val comb_B = thm "ATP_Linkup.COMBB_def";
 val comb_C = thm "ATP_Linkup.COMBC_def";
 val comb_S = thm "ATP_Linkup.COMBS_def";
-val comb_B' = thm "ATP_Linkup.COMBB'_def";
-val comb_C' = thm "ATP_Linkup.COMBC'_def";
-val comb_S' = thm "ATP_Linkup.COMBS'_def";
 val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
 val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
 
@@ -387,8 +380,7 @@
 val init_counters =
     Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
                  ("c_COMBB", 0), ("c_COMBC", 0),
-                 ("c_COMBS", 0), ("c_COMBB_e", 0),
-                 ("c_COMBC_e", 0), ("c_COMBS_e", 0)];
+                 ("c_COMBS", 0)];
 
 fun count_combterm (CombConst(c,tp,_), ct) =
      (case Symtab.lookup ct c of NONE => ct  (*no counter*)
@@ -421,15 +413,9 @@
         val S = if needed "c_COMBS"
                 then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
                 else []
-        val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e"
-                   then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C'])
-                   else []
-        val S' = if needed "c_COMBS_e"
-                 then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S'])
-                 else []
         val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
     in
-        map #2 (make_axiom_clauses thy (other @ IK @ BC @ S @ B'C' @ S'))
+        map #2 (make_axiom_clauses thy (other @ IK @ BC @ S))
     end;
 
 (*Find the minimal arity of each function mentioned in the term. Also, note which uses