# HG changeset patch
# User blanchet
# Date 1341956163 -7200
# Node ID 3a7ac7439ccf64ec2d32a83ad9d175d3c67994f6
# Parent  76759312b0b46faeafcbe70b29fc6c18e0e96d5b
tuning

diff -r 76759312b0b4 -r 3a7ac7439ccf src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -86,6 +86,7 @@
   val unproxify_const : string -> string
   val new_skolem_var_name_from_const : string -> string
   val atp_irrelevant_consts : string list
+  val atp_widely_irrelevant_consts : string list
   val atp_schematic_consts_of : term -> typ list Symtab.table
   val is_type_enc_higher_order : type_enc -> bool
   val is_type_enc_polymorphic : type_enc -> bool
@@ -399,7 +400,7 @@
    @{const_name conj}, @{const_name disj}, @{const_name implies},
    @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
 
-val atp_monomorph_bad_consts =
+val atp_widely_irrelevant_consts =
   atp_irrelevant_consts @
   (* These are ignored anyway by the relevance filter (unless they appear in
      higher-order places) but not by the monomorphizer. *)
@@ -411,7 +412,7 @@
   Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
 val add_schematic_consts_of =
   Term.fold_aterms (fn Const (x as (s, _)) =>
-                       not (member (op =) atp_monomorph_bad_consts s)
+                       not (member (op =) atp_widely_irrelevant_consts s)
                        ? add_schematic_const x
                       | _ => I)
 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
diff -r 76759312b0b4 -r 3a7ac7439ccf src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -446,8 +446,15 @@
       | _ => do_term false t
   in do_formula pos end
 
-(*Inserts a dummy "constant" referring to the theory name, so that relevance
-  takes the given theory into account.*)
+fun pconsts_in_fact thy is_built_in_const t =
+  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
+              (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
+                                                   (SOME true) t) []
+
+val const_names_in_fact = map fst ooo pconsts_in_fact
+
+(* Inserts a dummy "constant" referring to the theory name, so that relevance
+   takes the given theory into account. *)
 fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
                      : relevance_fudge) thy_name t =
   if exists (curry (op <) 0.0) [theory_const_rel_weight,
@@ -459,6 +466,13 @@
 fun theory_const_prop_of fudge th =
   theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
 
+fun pair_consts_fact thy is_built_in_const fudge fact =
+  case fact |> snd |> theory_const_prop_of fudge
+            |> pconsts_in_fact thy is_built_in_const of
+    [] => NONE
+  | consts => SOME ((fact, consts), NONE)
+
+
 (**** Constant / Type Frequencies ****)
 
 (* A two-dimensional symbol table counts frequencies of constants. It's keyed
@@ -597,19 +611,6 @@
         val res = rel_weight / (rel_weight + irrel_weight)
       in if Real.isFinite res then res else 0.0 end
 
-fun pconsts_in_fact thy is_built_in_const t =
-  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
-              (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
-                                                   (SOME true) t) []
-
-fun pair_consts_fact thy is_built_in_const fudge fact =
-  case fact |> snd |> theory_const_prop_of fudge
-            |> pconsts_in_fact thy is_built_in_const of
-    [] => NONE
-  | consts => SOME ((fact, consts), NONE)
-
-val const_names_in_fact = map fst ooo pconsts_in_fact
-
 type annotated_thm =
   (((unit -> string) * stature) * thm) * (string * ptype) list