# HG changeset patch
# User paulson
# Date 1129035816 -7200
# Node ID c82fb51ee18d96c80a094781c776e5c2662d4264
# Parent  b32fad049413d8815b60a33cb8d85eb5d49136a9
simplifying the treatment of nameless theorems

diff -r b32fad049413 -r c82fb51ee18d src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Oct 11 14:02:33 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Oct 11 15:03:36 2005 +0200
@@ -103,7 +103,6 @@
   sig
   val relevant : int ref
   val use_simpset: bool ref
-  val use_nameless: bool ref
   val get_clasimp_lemmas : 
          Proof.context -> term -> 
          (ResClause.clause * thm) Array.array * ResClause.clause list 
@@ -112,7 +111,6 @@
 structure ResClasimp : RES_CLASIMP =
 struct
 val use_simpset = ref false;   (*Performance is much better without simprules*)
-val use_nameless = ref true;
 
 val relevant = ref 0;  (*Relevance filtering is off by default*)
 
@@ -122,11 +120,14 @@
       (setmp print_mode [] 
 	(Pretty.setmp_margin 999 string_of_thm));
 	
+(*Returns the first substring enclosed in quotation marks, typically omitting 
+  the [.] of meta-level assumptions.*)
+val firstquoted = hd o (String.tokens (fn c => c = #"\""))
+	
 fun fake_thm_name th = 
-    Context.theory_name (theory_of_thm th) ^ "." ^ unenclose (plain_string_of_thm th);
+    Context.theory_name (theory_of_thm th) ^ "." ^ firstquoted (plain_string_of_thm th);
 
-fun put_name_pair ("",th) = if !use_nameless then (fake_thm_name th, th)
-                            else ("HOL.TrueI",TrueI)
+fun put_name_pair ("",th) = (fake_thm_name th, th)
   | put_name_pair (a,th)  = (a,th);
 
 (* outputs a list of (thm,clause) pairs *)
@@ -145,35 +146,27 @@
   FIXME: argument "goal" is a hack to allow relevance filtering.
   To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
 fun get_clasimp_lemmas ctxt goal = 
-    let val claset_rules = 
-              map put_name_pair
-	        (ReduceAxiomsN.relevant_filter (!relevant) goal 
-		  (ResAxioms.claset_rules_of_ctxt ctxt));
-	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs claset_rules []);
-
-	val simpset_rules =
-	      ReduceAxiomsN.relevant_filter (!relevant) goal 
-                (ResAxioms.simpset_rules_of_ctxt ctxt);
-	val named_simpset = map put_name_pair simpset_rules
-	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
-
-	val cls_thms = if !use_simpset then (claset_cls_thms@simpset_cls_thms) 
-	               else claset_cls_thms;
-	val cls_thms_list = List.concat cls_thms;
-	(*************************************************)
+    let val claset_cls_thms =
+              ResAxioms.clausify_rules_pairs
+		(map put_name_pair
+		  (ReduceAxiomsN.relevant_filter (!relevant) goal 
+		    (ResAxioms.claset_rules_of_ctxt ctxt)))
+	val simpset_cls_thms = 
+	      if !use_simpset then  
+		  ResAxioms.clausify_rules_pairs 
+		    (map put_name_pair 
+		      (ReduceAxiomsN.relevant_filter (!relevant) goal
+		        (ResAxioms.simpset_rules_of_ctxt ctxt))) 
+	      else []
+	val cls_thms_list = List.concat (claset_cls_thms@simpset_cls_thms)
 	(* Identify the set of clauses to be written out *)
-	(*************************************************)
 	val clauses = map #1(cls_thms_list);
 	val cls_nums = map ResClause.num_of_clauses clauses;
         val whole_list = List.concat 
               (map clause_numbering (ListPair.zip (cls_thms_list, cls_nums)));
- 
-        (*********************************************************)
-	(* create array and put clausename, number pairs into it *)
-	(*********************************************************)
-	val clause_arr = Array.fromList whole_list;
-  in
-	(clause_arr, clauses)
+ 	
+  in  (* create array of put clausename, number pairs into it *)
+      (Array.fromList whole_list, clauses)
   end;