# HG changeset patch
# User smolkas
# Date 1354101943 -3600
# Node ID 2f6035e858b61e57e0c91878cb1c5fce6505607d
# Parent  f066768743c7bb57dc6fad0061e41d8003ced241
fixed preplaying of case splits; incorperated new name of structure: Isabelle_Markup -> Markup

diff -r f066768743c7 -r 2f6035e858b6 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:25:43 2012 +0100
@@ -737,7 +737,7 @@
                      " (" ^ shrank_without_preplay_msg ^ ")"
                    else
                      "") 
-                ^ ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text
+                ^ ":\n" ^ Markup.markup Markup.sendback isar_text
             end
       end
     val isar_proof =
diff -r f066768743c7 -r 2f6035e858b6 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Nov 28 12:25:43 2012 +0100
@@ -137,7 +137,8 @@
             val premises =
               (case the succedent of
                 Prove (_, _, t, _) => t
-              | Assume (_, t) => t)
+              | Assume (_, t) => t
+              | _ => error "Internal error: unexpected succedent of case split")
                 ::  map ((fn Assume (_, a) => Logic.mk_implies(a, t)
                         | _ => error "Internal error: malformed case split") 
                         o hd) 
@@ -156,9 +157,9 @@
 
     (* cache metis preplay times in lazy time vector *)
     val metis_time =
-      v_map_index 
+      v_map_index
         (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout 
-          o apfst (fn i => try (get i proof_vect) ) o apsnd the)
+          o apfst (fn i => get i proof_vect) o apsnd the)
         proof_vect
     fun sum_up_time lazy_time_vector =
       Vector.foldl
@@ -187,7 +188,7 @@
             val s12 = merge s1 s2
             val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
           in
-            case try_metis_quietly timeout s12 () of
+            case try_metis_quietly timeout (NONE, s12) () of
               NONE => (NONE, metis_time)
             | some_t12 =>
               (SOME s12, metis_time