# HG changeset patch
# User blanchet
# Date 1387233414 -3600
# Node ID 79f66cd15d573ea1c1683056eea27d222bdb57ee
# Parent  f5fd4a34b0e8604323ff9ccf6970c75744f2bf2d
fixed source of 'Subscript' exception

diff -r f5fd4a34b0e8 -r 79f66cd15d57 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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 =
diff -r f5fd4a34b0e8 -r 79f66cd15d57 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- 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)