src/HOL/Tools/res_hol_clause.ML
 changeset 24943 5f5679e2ec2f parent 24940 8f9dea697b8d child 25008 38f4ecb71e8c
```     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Oct 10 15:05:34 2007 +0200
1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Oct 10 15:05:42 2007 +0200
1.3 @@ -2,10 +2,6 @@
1.4     Author: Jia Meng, NICTA
1.5
1.6  FOL clauses translated from HOL formulae.
1.7 -
1.8 -The combinator code needs to be deleted after the translation paper has been published.
1.9 -It cannot be used with proof reconstruction because combinators are not introduced by proof.
1.10 -The Turner combinators (B', C', S') yield no improvement and should be deleted.
1.11  *)
1.12
1.13  signature RES_HOL_CLAUSE =
1.14 @@ -49,9 +45,6 @@
1.15  val comb_B = thm "ATP_Linkup.COMBB_def";
1.16  val comb_C = thm "ATP_Linkup.COMBC_def";
1.17  val comb_S = thm "ATP_Linkup.COMBS_def";
1.18 -val comb_B' = thm "ATP_Linkup.COMBB'_def";
1.19 -val comb_C' = thm "ATP_Linkup.COMBC'_def";
1.20 -val comb_S' = thm "ATP_Linkup.COMBS'_def";
1.21  val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
1.22  val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
1.23
1.24 @@ -387,8 +380,7 @@
1.25  val init_counters =
1.26      Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
1.27                   ("c_COMBB", 0), ("c_COMBC", 0),
1.28 -                 ("c_COMBS", 0), ("c_COMBB_e", 0),
1.29 -                 ("c_COMBC_e", 0), ("c_COMBS_e", 0)];
1.30 +                 ("c_COMBS", 0)];
1.31
1.32  fun count_combterm (CombConst(c,tp,_), ct) =
1.33       (case Symtab.lookup ct c of NONE => ct  (*no counter*)
1.34 @@ -421,15 +413,9 @@
1.35          val S = if needed "c_COMBS"
1.36                  then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
1.37                  else []
1.38 -        val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e"
1.39 -                   then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C'])
1.40 -                   else []
1.41 -        val S' = if needed "c_COMBS_e"
1.42 -                 then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S'])
1.43 -                 else []
1.44          val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
1.45      in
1.46 -        map #2 (make_axiom_clauses thy (other @ IK @ BC @ S @ B'C' @ S'))
1.47 +        map #2 (make_axiom_clauses thy (other @ IK @ BC @ S))
1.48      end;
1.49
1.50  (*Find the minimal arity of each function mentioned in the term. Also, note which uses
```