--- 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 =