remove_all_simps xs name_rules'

                                   remove_all_simps xs name_rules'

                               end; 

                               end; 

 fun get_simp_metas [] = [[]]

 fun get_simp_metas [] = [[]]

 |   get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x

 |   get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x

                              in

                              in

                                  metas::(get_simp_metas xs)

                                  metas::(get_simp_metas xs)

                              end

                              end

                                     (* get (name, thm) pairs for claset rules *)

                                     (* get (name, thm) pairs for claset rules *)

                                    (*******************************************)

                                    (*******************************************)

                                    val names_rules = ListPair.zip (good_names,name_fol_cs);

                                    val names_rules = ListPair.zip (good_names,name_fol_cs);

                                    val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;

                                    val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;

                                    (* list of lists of tptp string clauses *)

                                    (* list of lists of tptp string clauses *)

                                    val stick_clasrls =  map stick claset_tptp_strs;

                                    val stick_clasrls =  map stick claset_tptp_strs;

                                   val named_simps = List.filter has_name_pair simpset_name_rules;

                                   val named_simps = List.filter has_name_pair simpset_name_rules;

                                   val simp_names = map #1 named_simps;

                                   val simp_names = map #1 named_simps;

                                   val simp_rules = map #2 named_simps;

                                   val simp_rules = map #2 named_simps;

                                  (* 1137 clausif simps *)

                                  (* 1137 clausif simps *)

                                     val simp_names = map #1 name_fol_simps;

                                     val simp_names = map #1 name_fol_simps;

                                     val simp_rules = map #2 name_fol_simps;

                                     val simp_rules = map #2 name_fol_simps;

                                      (* 995 of these *)

                                      (* 995 of these *)

                                     (* need to get names of claset_cluases so we can make sure we've*)

                                     (* need to get names of claset_cluases so we can make sure we've*)

                                     (* got the same ones (ie. the named ones ) as the claset rules *)

                                     (* got the same ones (ie. the named ones ) as the claset rules *)

                                     (* length 1374*)

                                     (* length 1374*)

                                     val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;

                                     val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;

                                     val stick_strs = map stick simpset_tptp_strs;

                                     val stick_strs = map stick simpset_tptp_strs;

                                     val name_stick = ListPair.zip (simp_names,stick_strs);

                                     val name_stick = ListPair.zip (simp_names,stick_strs);