src/HOL/Tools/ATP/res_clasimpset.ML
changeset 15872 8336ff711d80
parent 15789 4cb16144c81b
child 15907 f377ba412dba
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Apr 28 17:08:08 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Apr 28 17:56:58 2005 +0200
     1.3 @@ -170,9 +170,6 @@
     1.4  
     1.5  
     1.6  
     1.7 -fun thm_is_fol (x, thm) = rule_is_fol thm
     1.8 -
     1.9 -
    1.10  fun get_simp_metas [] = [[]]
    1.11  |   get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x
    1.12                               in
    1.13 @@ -208,7 +205,7 @@
    1.14  
    1.15                                     val names_rules = ListPair.zip (good_names,name_fol_cs);
    1.16                                     
    1.17 -                                   val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[])
    1.18 +                                   val new_clasrls = #1(ResAxioms.clausify_rules name_fol_cs[])
    1.19  
    1.20                                     val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
    1.21  
    1.22 @@ -251,11 +248,10 @@
    1.23                                    val simp_names = map #1 named_simps;
    1.24                                    val simp_rules = map #2 named_simps;
    1.25                                
    1.26 -                                  val (simpset_cls,badthms) = ResAxioms.clausify_simpset_rules simp_rules [];
    1.27 +                                  val (simpset_cls,badthms) = ResAxioms.clausify_rules  simp_rules [];
    1.28                                   (* 1137 clausif simps *)
    1.29 -                                  val clausifiable_simps = remove_all_simps badthms named_simps;
    1.30 +                                  val name_fol_simps = remove_all_simps badthms named_simps;
    1.31                                     
    1.32 -                                    val name_fol_simps = List.filter thm_is_fol clausifiable_simps ;
    1.33                                      val simp_names = map #1 name_fol_simps;
    1.34                                      val simp_rules = map #2 name_fol_simps;
    1.35                                      
    1.36 @@ -263,7 +259,7 @@
    1.37                                      (* need to get names of claset_cluases so we can make sure we've*)
    1.38                                      (* got the same ones (ie. the named ones ) as the claset rules *)
    1.39                                      (* length 1374*)
    1.40 -                                    val new_simps = #1(ResAxioms.clausify_simpset_rules simp_rules []);
    1.41 +                                    val new_simps = #1(ResAxioms.clausify_rules  simp_rules []);
    1.42                                      val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
    1.43  
    1.44                                      val stick_strs = map stick simpset_tptp_strs;