# HG changeset patch
# User paulson
# Date 1115033448 -7200
# Node ID f377ba412dbaf3a62e8fb0f7656746a73bfd42f7
# Parent  9cb0a8ffa40da508ede1004ba43d3d0ecfe4ebbe
deleted redundant code

diff -r 9cb0a8ffa40d -r f377ba412dba src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Mon May 02 13:30:36 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Mon May 02 13:30:48 2005 +0200
@@ -5,22 +5,8 @@
 
 (* Get claset rules *)
 
-
-
-fun remove_all [] rules = rules
-|   remove_all (x::xs) rules = let val rules' = List.filter (not_equal x) rules
-                              in
-                                  remove_all xs rules'
-                              end; 
-
 fun has_name th = not((Thm.name_of_thm th)= "")
 
-fun rule_is_fol th = let val tm = prop_of th
-                     in 
-                        Term.is_first_order tm
-                     end
-
-
 fun has_name_pair (a,b) = not_equal a "";
 fun good_pair c (a,b) = not_equal b c;
 
@@ -30,11 +16,9 @@
 val clause_arr = Array.array(3500, ("empty", 0));
 
 
+(*
 val foo_arr = Array.array(20, ("a",0));
 
-
-(*
-
 fill_cls_array foo_arr 0 [("b",1), ("c",2), ("d", 3), ("e", 4), ("f",5)];
 
 
@@ -155,19 +139,6 @@
 fun memo_find_clause name = case Symtab.lookup (!nc,name) of
       	        NONE =>  []
                 |SOME cls  => cls ;
-      	        	
-
-
-
-fun not_second c (a,b)  = not_equal b c;
-
-fun remove_all_simps [] name_rule_list:(string*thm) list = name_rule_list
-|   remove_all_simps ((x:thm)::xs) (name_rule_list:(string*thm) list) = 
-                              let val name_rules' = List.filter (not_second  x) name_rule_list
-                              in
-                                  remove_all_simps xs name_rules'
-                              end; 
-
 
 
 fun get_simp_metas [] = [[]]
@@ -184,18 +155,12 @@
                                
 
 fun write_out_clasimp filename (clause_arr:(string * int) Array.array)  = let 
-                                  val  outfile = TextIO.openOut("wibble");                                  val _ = TextIO.output (outfile, ("in write_out_clasimpset"))
-                                  val _ =  TextIO.closeOut outfile
-                                   val _= (warning ("in writeoutclasimp"))
+                                   val _= warning "in writeoutclasimp"
                                    (****************************************)
                                    (* add claset rules to array and write out as strings *)
                                    (****************************************)
-                                   val claset_rules = ResAxioms.claset_rules_of_thy (the_context())
-                                   val claset = ResAxioms.clausify_classical_rules_thy (the_context())
-                                   val (claset_clauses,badthms) =  claset;
-                                   val clausifiable_rules = remove_all badthms claset_rules;
-                                   val named_claset = List.filter has_name clausifiable_rules;
-                                   val name_fol_cs = List.filter rule_is_fol  named_claset;
+                                   val clausifiable_rules = ResAxioms.claset_rules_of_thy (the_context())
+                                   val name_fol_cs = List.filter has_name clausifiable_rules;
                                    (* length name_fol_cs is 93 *)
                                    val good_names = map Thm.name_of_thm name_fol_cs;
  
@@ -248,14 +213,8 @@
                                   val simp_names = map #1 named_simps;
                                   val simp_rules = map #2 named_simps;
                               
-                                  val (simpset_cls,badthms) = ResAxioms.clausify_rules  simp_rules [];
                                  (* 1137 clausif simps *)
-                                  val name_fol_simps = remove_all_simps badthms named_simps;
                                    
-                                    val simp_names = map #1 name_fol_simps;
-                                    val simp_rules = map #2 name_fol_simps;
-                                    
-                                     (* 995 of these *)
                                     (* 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 *)
                                     (* length 1374*)