--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Dec 16 23:05:16 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Dec 16 23:36:54 2013 +0100
@@ -108,13 +108,17 @@
tag_list 1 facts
|> map (fn (j, fact) => fact |> apsnd (K j))
|> filter_used_facts false used_facts
+ |> distinct (eq_fst (op =))
|> map (prefix "@" o string_of_int o snd)
fun filter_info (fact_filter, facts) =
let
val indices = find_indices facts
- val unknowns = replicate (num_used_facts - length indices) "?"
- in (commas (indices @ unknowns), fact_filter) end
+ (* "Int.max" is there for robustness -- it shouldn't be necessary *)
+ val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?"
+ in
+ (commas (indices @ unknowns), fact_filter)
+ end
val filter_infos =
map filter_info (("actual", used_from) :: factss)