--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Dec 16 23:05:16 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Dec 16 23:36:54 2013 +0100
@@ -394,8 +394,7 @@
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
fun filter_used_facts keep_chained used =
- filter ((member (op =) used o fst) orf
- (if keep_chained then is_fact_chained else K false))
+ filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
fun play_one_line_proof mode debug verbose timeout pairs state i preferred
reconstrs =
--- 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)