1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Tue Jan 15 12:45:19 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Tue Jan 15 16:34:19 2013 +0100
     1.3 @@ -68,8 +68,8 @@
     1.4        val metis_fail = ref false
     1.5      in
     1.6        fun handle_metis_fail try_metis () =
     1.7 -        try_metis () handle exp =>
     1.8 -          (if Exn.is_interrupt exp orelse debug then reraise exp 
     1.9 +        try_metis () handle exn =>
    1.10 +          (if Exn.is_interrupt exn orelse debug then reraise exn
    1.11             else metis_fail := true; SOME Time.zeroTime)
    1.12        fun get_time lazy_time =
    1.13          if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time