# HG changeset patch
# User blanchet
# Date 1282832320 -7200
# Node ID d0f98bd81a8546fc3d8d99e24baa64571b448afc
# Parent  71c9f61516cdaddcd64d6dc99633312fd4dfd50f
add nameless chained facts to the pool of things known to Sledgehammer

diff -r 71c9f61516cd -r d0f98bd81a85 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 14:58:45 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 16:18:40 2010 +0200
@@ -68,11 +68,11 @@
 (*An abstraction of Isabelle types*)
 datatype pseudotype = PVar | PType of string * pseudotype list
 
-fun string_for_pseudotype PVar = "?"
+fun string_for_pseudotype PVar = "_"
   | string_for_pseudotype (PType (s, Ts)) =
     (case Ts of
        [] => ""
-     | [T] => string_for_pseudotype T
+     | [T] => string_for_pseudotype T ^ " "
      | Ts => string_for_pseudotypes Ts ^ " ") ^ s
 and string_for_pseudotypes Ts =
   "(" ^ commas (map string_for_pseudotype Ts) ^ ")"
@@ -318,7 +318,7 @@
     trace_msg (fn () => "Number of candidates: " ^
                         string_of_int (length candidates));
     trace_msg (fn () => "Effective threshold: " ^
-                        Real.toString (#2 (hd accepts)));
+                        Real.toString (#2 (List.last accepts)));
     trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^
         "): " ^ (accepts
                  |> map (fn ((((name, _), _), _), weight) =>
@@ -597,11 +597,12 @@
     (* Unnamed nonchained formulas with schematic variables are omitted, because
        they are rejected by the backticks (`...`) parser for some reason. *)
     fun is_good_unnamed_local th =
+      not (Thm.has_name_hint th) andalso
+      (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) andalso
       forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
-      andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))
     val unnamed_locals =
-      local_facts |> Facts.props |> filter is_good_unnamed_local
-                  |> map (pair "" o single)
+      union Thm.eq_thm (Facts.props local_facts) chained_ths
+      |> filter is_good_unnamed_local |> map (pair "" o single)
     val full_space =
       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
     fun add_facts global foldx facts =