src/HOL/Tools/res_atp.ML
changeset 20757 fe84fe0dfd30
parent 20661 46832fee1215
child 20781 e26fe5c63c2f
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Sep 28 06:21:06 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Sep 28 11:04:41 2006 +0200
     1.3 @@ -481,10 +481,17 @@
     1.4  fun banned_thmlist s =
     1.5    (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
     1.6  
     1.7 +(*Reject theorems with names like "List.filter.filter_list_def" or
     1.8 +  "Accessible_Part.acc.defs", as these are definitions arising from packages*)
     1.9 +fun is_package_def a =
    1.10 +  let val l = NameSpace.unpack a
    1.11 +  in  length l > 2 andalso String.isSubstring "def" (List.last l)  end;
    1.12 +
    1.13  fun make_banned_test xs = 
    1.14    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
    1.15                                  (6000, HASH_STRING)
    1.16 -      fun banned_aux s = isSome (Polyhash.peek ht s) orelse banned_thmlist s
    1.17 +      fun banned_aux s = 
    1.18 +            isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s
    1.19        fun banned s = exists banned_aux (delete_numeric_suffix s)
    1.20    in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
    1.21        app (insert_suffixed_names ht) (!blacklist @ xs); 
    1.22 @@ -661,7 +668,6 @@
    1.23  			  | Fol => FOL
    1.24  			  | Hol => HOL
    1.25  	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
    1.26 -	val user_lemmas_names = map #1 user_rules
    1.27  	val cla_simp_atp_clauses = included_thms |> blacklist_filter
    1.28  	                             |> make_unique |> ResAxioms.cnf_rules_pairs
    1.29                                       |> restrict_to_logic logic 
    1.30 @@ -673,11 +679,12 @@
    1.31  	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
    1.32  	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
    1.33          val writer = if dfg then dfg_writer else tptp_writer 
    1.34 -	val file = atp_input_file()
    1.35 +	and file = atp_input_file()
    1.36 +	and user_lemmas_names = map #1 user_rules
    1.37      in
    1.38 -	(writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
    1.39 -	 Output.debug ("Writing to " ^ file);
    1.40 -	 file)
    1.41 +	writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
    1.42 +	Output.debug ("Writing to " ^ file);
    1.43 +	file
    1.44      end;
    1.45  
    1.46