1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 09 15:48:34 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 09 20:29:50 2013 +0100
     1.3 @@ -69,7 +69,8 @@
     1.4      in
     1.5        fun handle_metis_fail try_metis () =
     1.6          try_metis () handle exp =>
     1.7 -          (if debug then raise exp else metis_fail := true; SOME Time.zeroTime)
     1.8 +          (if Exn.is_interrupt exp orelse debug then reraise exp 
     1.9 +           else metis_fail := true; SOME Time.zeroTime)
    1.10        fun get_time lazy_time =
    1.11          if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
    1.12        val metis_fail = fn () => !metis_fail
    1.13 @@ -208,11 +209,12 @@
    1.14                  (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
    1.15                    (fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
    1.16                | (Obtain(qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
    1.17 -                  (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2) )
    1.18 +                  (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
    1.19 +              | _ => error "Internal error: unmergeable Isar steps" )
    1.20              val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
    1.21              val gfs = union (op =) gfs1 gfs2
    1.22            in step_constructor (By_Metis (lfs, gfs)) end
    1.23 -        | merge _ _ = error "Internal error: Unmergeable Isar steps"
    1.24 +        | merge _ _ = error "Internal error: unmergeable Isar steps"
    1.25  
    1.26        fun try_merge metis_time (s1, i) (s2, j) =
    1.27          (case get i metis_time |> Lazy.force of