# HG changeset patch
# User paulson
# Date 1127463967 -7200
# Node ID cd555d5a32543b7a72b676643a9118ce3b640277
# Parent  3e3a30bf702f9e5a6ac216c5ea75eabe60f18a79
changed defaults

diff -r 3e3a30bf702f -r cd555d5a3254 src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Sep 23 10:25:55 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Sep 23 10:26:07 2005 +0200
@@ -22,10 +22,8 @@
 
 fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
 
-
 fun thm_consts_rm ncs thm = term_consts_rm ncs (prop_of thm);
 
-
 fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm;
 
 fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
@@ -33,8 +31,6 @@
 fun make_pairs [] _ = []
   | make_pairs (x::xs) y = (x,y)::(make_pairs xs y);
 
-
-
 fun const_thm_list_aux [] cthms = cthms
   | const_thm_list_aux (thm::thms) cthms =
     let val consts = consts_of_thm thm
@@ -80,12 +76,10 @@
 
     in  relevant_axioms_aux1 consts 1  end;
 
-
 fun relevant_filter n goal thms = 
     if n<=0 then thms 
     else #2 (relevant_axioms goal (make_thm_table thms) n);
 
-
 (* find the thms from thy that contain relevant constants, n is the iteration number *)
 fun find_axioms_n thy goal n =
     let val clasetR = ResAxioms.claset_rules_of_thy thy
@@ -95,7 +89,6 @@
 	relevant_axioms goal table n
     end;
 
-
 fun find_axioms_n_c thy goal n =
     let val current_thms = PureThy.thms_of thy
 	val table = make_thm_table current_thms
@@ -119,7 +112,7 @@
 structure ResClasimp : RES_CLASIMP =
 struct
 val use_simpset = ref false;   (*Performance is much better without simprules*)
-val use_nameless = ref false;  (*Because most are useless [iff] rules*)
+val use_nameless = ref true;
 
 val relevant = ref 0;  (*Relevance filtering is off by default*)
 
@@ -136,9 +129,6 @@
                             else ("HOL.TrueI",TrueI)
   | put_name_pair (a,th)  = (a,th);
 
-(* changed, now it also finds out the name of the theorem. *)
-(* convert a theorem into CNF and then into Clause.clause format. *)
-
 (* outputs a list of (thm,clause) pairs *)
 
 fun multi x 0 xlist = xlist