# HG changeset patch
# User smolkas
# Date 1367830988 -7200
# Node ID 71052c42edf22ea9679f74271af36c3dafe0f5a0
# Parent  724c67f59929bbfa69835f5877da010a68d570fa
avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug

diff -r 724c67f59929 -r 71052c42edf2 src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Mon May 06 11:03:08 2013 +0200
@@ -134,8 +134,8 @@
         if p <> cp then
           (env, cp + 1, ps, annots)
         else
-          let val (_, (env', T')) = get_annot env T in
-            (env', cp + 1, ps', (p, T') :: annots)
+          let val (annot_necessary, (env', T')) = get_annot env T in
+            (env', cp + 1, ps', annots |> annot_necessary ? cons (p, T'))
           end
       | post1 _ _ accum = accum
     val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'
diff -r 724c67f59929 -r 71052c42edf2 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Mon May 06 11:03:08 2013 +0200
@@ -170,6 +170,7 @@
         if Inttab.is_empty cand_tab
           orelse n_metis' <= target_n_metis
           orelse (on_top_level andalso n'<3)
+          orelse metis_fail()
         then
           (Vector.foldr
              (fn (NONE, steps) => steps | (SOME s, steps) => s :: steps)
@@ -187,12 +188,14 @@
               merge_steps metis_time step_vect refed_by cand_tab n' n_metis'
             | (s, metis_time) =>
             let
-              val refs = refs s1
+              val refs_s1 = refs s1
               val refed_by = refed_by |> fold
-                (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
+                (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j))
+                refs_s1
+              val shared_refs = Ord_List.inter int_ord refs_s1 (refs s2)
               val new_candidates =
                 fold (add_if_cand step_vect)
-                  (map (fn i => (i, get i refed_by)) refs) []
+                  (map (fn i => (i, get i refed_by)) shared_refs) []
               val cand_tab = add_list cand_tab new_candidates
               val step_vect = step_vect |> replace NONE i |> replace s j
             in