tuned
* * *
easier debugging
* * *
tuned

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Fri Jul 12 19:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Fri Jul 12 19:54:36 2013 +0200
@@ -7,8 +7,8 @@
 Minimal: Reducing the set of constraints further will make it incomplete.
 
 When configuring the pretty printer appropriately, the constraints will show up
-as type annotations when printing the term. This allows the term to be reparsed
-without a change of types.
+as type annotations when printing the term. This allows the term to be printed
+and reparsed without a change of types.
 
 NOTE: Terms should be unchecked before calling annotate_types to avoid awkward
 syntax.
@@ -87,6 +87,7 @@
     val get_types = post_fold_term_type (K cons) []
   in
     fold (Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty
+    handle Type.TYPE_MATCH => raise Fail "Sledgehammer_Annotate: match_types"
   end
 
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 19:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 19:54:36 2013 +0200
@@ -164,7 +164,7 @@
     fun tac {context = ctxt, prems = _} =
       HEADGOAL (tac_of_method proof_method type_enc lam_trans ctxt facts)
     fun run_tac () = goal tac
-      handle ERROR msg => error ("preplay error: " ^ msg)
+      handle ERROR msg => error ("Preplay error: " ^ msg)
     val preplay_time = take_time timeout run_tac ()
   in
     (* tracing *)
@@ -234,16 +234,22 @@
       (* add local proof facts to context *)
       val ctxt = enrich_context proof ctxt
 
-      fun preplay timeout step =
+      fun preplay quietly timeout step =
         preplay_raw debug preplay_trace type_enc lam_trans ctxt timeout step
         |> PplSucc
         handle exn =>
-          if Exn.is_interrupt exn orelse debug then reraise exn
-          else PplFail exn
+          if Exn.is_interrupt exn then
+            reraise exn
+          else if not quietly andalso debug then
+            (warning ("Preplay failure:\n  " ^ @{make_string} step ^ "\n  "
+                      ^ @{make_string} exn);
+             PplFail exn)
+          else
+            PplFail exn
 
       (* preplay steps treating exceptions like timeouts *)
       fun preplay_quietly timeout step =
-        case preplay timeout step of
+        case preplay true timeout step of
           PplSucc preplay_time => preplay_time
         | PplFail _ => (true, timeout)
 
@@ -254,7 +260,7 @@
               NONE => tab
             | SOME l =>
                 Canonical_Lbl_Tab.update_new
-                  (l, (fn () => preplay preplay_timeout step) |> Lazy.lazy)
+                  (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy)
                   tab
             handle Canonical_Lbl_Tab.DUP _ =>
               raise Fail "Sledgehammer_Preplay: preplay time table"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Jul 12 19:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Jul 12 19:54:36 2013 +0200
@@ -170,7 +170,7 @@
     fun do_byline by (_, subst) =
       by |> map_facts_of_byline (apfst (map (AList.lookup (op =) subst #> the)))
     handle Option.Option =>
-      raise Fail "Sledgehammer_Compress: relabel_proof_canonically"
+      raise Fail "Sledgehammer_Proof: relabel_proof_canonically"
 
     fun do_assm (l, t) state =
       let