# HG changeset patch
# User paulson
# Date 1143795140 -7200
# Node ID 9e82f341a71b797c633c7e9e821620aa603d089a
# Parent  96ca738055a632e8a4b127b2a98fa730e6596a74
Removal of unused code

diff -r 96ca738055a6 -r 9e82f341a71b src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Tue Mar 28 16:48:18 2006 +0200
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Fri Mar 31 10:52:20 2006 +0200
@@ -6,12 +6,7 @@
 struct
 
 val pass_mark = ref 0.6;
-val reduction_factor = ref 1.0;
-val convergence = ref 4.0;   (*Higher numbers allow longer inference chains*)
-
-(*FIXME DELETE Whether all "simple" unit clauses should be included*)
-val add_unit = ref false;
-val unit_pass_mark = ref 0.0;
+val convergence = ref 1.6;   (*Higher numbers allow longer inference chains*)
 
 (*The default ignores the constant-count and gives the old Strategy 3*)
 val weight_fn = ref (fn x : real => 1.0);
@@ -24,28 +19,6 @@
    "op =","==","True","False"];
 
 
-(*** unit clauses ***)
-datatype clause_kind = Unit_neq | Unit_geq | Other
-
-
-fun literals_of_term args (Const ("Trueprop",_) $ P) = literals_of_term args P
-  | literals_of_term args (Const ("op |",_) $ P $ Q) = 
-    literals_of_term (literals_of_term args P) Q
-  | literals_of_term args P = P::args;
-
-fun is_ground t = (term_vars t = []) andalso (term_frees t = []);
-
-fun eq_clause_type (P,Q) = 
-    if ((is_ground P) orelse (is_ground Q)) then Unit_geq else Other;
-
-fun unit_clause_type (Const ("op =",_) $ P $ Q) = eq_clause_type (P,Q)
-  | unit_clause_type _ = Unit_neq;
-
-fun clause_kind tm = 
-    case literals_of_term [] tm of
-        [lit] => unit_clause_type lit
-      | _ => Other;
-
 (*** constants with types ***)
 
 (*An abstraction of Isabelle types*)
@@ -78,7 +51,7 @@
 (*Free variables are counted, as well as constants, to handle locales*)
 fun add_term_consts_typs_rm thy (Const(c, typ)) cs =
       if (c mem standard_consts) then cs 
-      else const_with_typ thy (c,typ) ins cs
+      else const_with_typ thy (c,typ) ins cs   (*suppress multiples*)
   | add_term_consts_typs_rm thy (Free(c, typ)) cs =
       const_with_typ thy (c,typ) ins cs
   | add_term_consts_typs_rm thy (t $ u) cs =
@@ -172,20 +145,8 @@
 	    end
     in  Output.debug ("relevant_clauses: " ^ Real.toString p);
         relevant ([],[]) end;
-
-(*Unit clauses other than non-trivial equations can be included subject to
-  a separate (presumably lower) mark. *)
-fun good_unit_clause ((t,_), (_,w)) = 
-     !unit_pass_mark <= w andalso
-     (case clause_kind t of
-	  Unit_neq => true
-	| Unit_geq => true
-	| Other => false);
 	
-fun showconst (c,cttab) = 
-      List.app (fn n => Output.debug (Int.toString n ^ " occurrences of " ^ c))
-	        (map #2 (CTtab.dest cttab))
-	      
+     
 exception ConstFree;
 fun dest_ConstFree (Const aT) = aT
   | dest_ConstFree (Free aT) = aT