fixed source of 'Subscript' exception
authorblanchet
Mon, 16 Dec 2013 23:36:54 +0100
changeset 54773 79f66cd15d57
parent 54772 f5fd4a34b0e8
child 54774 bddb91fb8e37
fixed source of 'Subscript' exception
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.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 =
--- 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)