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