# HG changeset patch
# User paulson
# Date 1159434281 -7200
# Node ID fe84fe0dfd305f0cf36c8232b937f4c557186fe3
# Parent  fec7f5834ffe6169afcdb1a989167a4574902fae
Definitions produced by packages are now blacklisted.

diff -r fec7f5834ffe -r fe84fe0dfd30 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Sep 28 06:21:06 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Sep 28 11:04:41 2006 +0200
@@ -481,10 +481,17 @@
 fun banned_thmlist s =
   (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
 
+(*Reject theorems with names like "List.filter.filter_list_def" or
+  "Accessible_Part.acc.defs", as these are definitions arising from packages*)
+fun is_package_def a =
+  let val l = NameSpace.unpack a
+  in  length l > 2 andalso String.isSubstring "def" (List.last l)  end;
+
 fun make_banned_test xs = 
   let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
                                 (6000, HASH_STRING)
-      fun banned_aux s = isSome (Polyhash.peek ht s) orelse banned_thmlist s
+      fun banned_aux s = 
+            isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s
       fun banned s = exists banned_aux (delete_numeric_suffix s)
   in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
       app (insert_suffixed_names ht) (!blacklist @ xs); 
@@ -661,7 +668,6 @@
 			  | Fol => FOL
 			  | Hol => HOL
 	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
-	val user_lemmas_names = map #1 user_rules
 	val cla_simp_atp_clauses = included_thms |> blacklist_filter
 	                             |> make_unique |> ResAxioms.cnf_rules_pairs
                                      |> restrict_to_logic logic 
@@ -673,11 +679,12 @@
 	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
         val writer = if dfg then dfg_writer else tptp_writer 
-	val file = atp_input_file()
+	and file = atp_input_file()
+	and user_lemmas_names = map #1 user_rules
     in
-	(writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
-	 Output.debug ("Writing to " ^ file);
-	 file)
+	writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
+	Output.debug ("Writing to " ^ file);
+	file
     end;