# HG changeset patch
# User paulson
# Date 1122047029 -7200
# Node ID 74eddde1de2ff2eac83c7c65a4a43360bc5a25d9
# Parent  fa26952fa7b630231f35cb182934cfa81335dae6
dead code removal

diff -r fa26952fa7b6 -r 74eddde1de2f src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jul 22 17:43:03 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jul 22 17:43:49 2005 +0200
@@ -110,8 +110,6 @@
   val relevant : int ref
   val write_out_clasimp : string -> theory -> term -> 
                              (ResClause.clause * thm) Array.array * int
-  val write_out_clasimp_small :
-     string -> theory -> (ResClause.clause * thm) Array.array * int
   end;
 
 structure ResClasimp : RES_CLASIMP =
@@ -179,7 +177,8 @@
     end;
 
 (*Write out the claset and simpset rules of the supplied theory.
-  FIXME: argument "goal" is a hack to allow relevance filtering.*)
+  FIXME: argument "goal" is a hack to allow relevance filtering.
+  To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
 fun write_out_clasimp filename thy goal = 
     let val claset_rules = 
               ReduceAxiomsN.relevant_filter (!relevant) goal 
@@ -223,53 +222,6 @@
 	(clause_arr, num_of_clauses)
   end;
 
-
-
-
-
-(*Write out the claset and simpset rules of the supplied theory. Only include the first 50 rules*)
-fun write_out_clasimp_small filename thy = 
-    let val claset_rules = ResAxioms.claset_rules_of_thy thy;
-	val named_claset = List.filter has_name_pair claset_rules;
-	val claset_names = map remove_spaces_pair (named_claset)
-	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
-
-	val simpset_rules = ResAxioms.simpset_rules_of_thy thy;
-	val named_simpset = 
-	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
-	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
-
-	val cls_thms = (claset_cls_thms@simpset_cls_thms);
-	val cls_thms_list = List.concat cls_thms;
-        (* length 1429 *)
-	(*************************************************)
-	(* Write out clauses as tptp strings to filename *)
-	(*************************************************)
-	val clauses = map #1(cls_thms_list);
-	val cls_tptp_strs = map ResClause.tptp_clause clauses;
-        val alllist = pairup cls_thms_list cls_tptp_strs
-        val whole_list = List.concat (map clause_numbering alllist);
-        val mini_list = List.take ( whole_list,50)
-        (*********************************************************)
-	(* create array and put clausename, number pairs into it *)
-	(*********************************************************)
-	val num_of_clauses =  0;
-	val clause_arr = Array.fromList mini_list;
-	val num_of_clauses = List.length mini_list;
-
-	(* list of lists of tptp string clauses *)
-	val stick_clasrls =   List.concat cls_tptp_strs;
-        (* length 1581*)
-	val out = TextIO.openOut filename;
-	val _=   ResLib.writeln_strs out (List.take (stick_clasrls,50));
-	val _= TextIO.flushOut out;
-	val _= TextIO.closeOut out
-  in
-	(clause_arr, num_of_clauses)
-  end;
-
-
-
 end;