# HG changeset patch
# User paulson
# Date 1158142895 -7200
# Node ID 958ec4833d87c8ec81268bedff5dfc13c0a09698
# Parent  756c4f1fd04c42645f4b7ee947f968a9dbaf8c5c
Added the "theory_const" option. Only it is OFF because it's often harmful!

diff -r 756c4f1fd04c -r 958ec4833d87 src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Sep 13 12:20:21 2006 +0200
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Sep 13 12:21:35 2006 +0200
@@ -12,6 +12,7 @@
 struct
 
 val run_relevance_filter = ref true;
+val theory_const = ref false;
 val pass_mark = ref 0.6;
 val convergence = ref 2.4;   (*Higher numbers allow longer inference chains*)
 val follow_defs = ref false;  (*Follow definitions. Makes problems bigger.*)
@@ -24,10 +25,10 @@
 
 
 (*Including equality in this list might be expected to stop rules like subset_antisym from
-  being chosen, but for some reason filtering works better with them listed.*)
-val standard_consts =
-  ["Trueprop","==>","all","==","All","Ex","Ball","Bex","op &","op |","Not","op -->",
-   "op =","True","False"];
+  being chosen, but for some reason filtering works better with them listed. The
+  logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
+  must be within comprehensions.*)
+val standard_consts = ["Trueprop","==>","all","==","op |","Not","op ="];
 
 
 (*** constants with types ***)
@@ -83,6 +84,14 @@
 
 fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab;
 
+(*Inserts a dummy "constant" referring to the theory name, so that relevance
+  takes the given theory into account.*)
+fun const_prop_of th =
+ if !theory_const then
+  let val name = Context.theory_name (theory_of_thm th)
+      val t = Const (name ^ ". 1", HOLogic.boolT)
+  in  t $ prop_of th  end
+ else prop_of th;
 
 (**** Constant / Type Frequencies ****)
 
@@ -116,7 +125,7 @@
 	    count_term_consts (t, count_term_consts (u, tab))
 	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
 	| count_term_consts (_, tab) = tab
-  in  count_term_consts (prop_of thm, tab)  end;
+  in  count_term_consts (const_prop_of thm, tab)  end;
 
 
 (******** filter clauses ********)
@@ -151,7 +160,7 @@
   in  Symtab.fold add_expand_pairs tab []  end;
 
 fun pair_consts_typs_axiom thy (thm,name) =
-    ((thm,name), (consts_typs_of_term thy (prop_of thm)));
+    ((thm,name), (consts_typs_of_term thy (const_prop_of thm)));
 
 exception ConstFree;
 fun dest_ConstFree (Const aT) = aT