1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 09 20:29:50 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 09 20:46:32 2013 +0100
     1.3 @@ -126,7 +126,7 @@
     1.4            |> maps (thms_of_name ctxt)
     1.5  
     1.6        (* TODO: add "Obtain" case *)
     1.7 -      exception ZeroTime
     1.8 +      exception ZEROTIME
     1.9        fun try_metis timeout (succedent, step) =
    1.10          (if not preplay then K (SOME Time.zeroTime) else
    1.11            let
    1.12 @@ -158,7 +158,7 @@
    1.13                  in
    1.14                    (prop, byline, true)
    1.15                  end
    1.16 -              | _ => raise ZeroTime)
    1.17 +              | _ => raise ZEROTIME)
    1.18              val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    1.19              val facts =
    1.20                (case byline of
    1.21 @@ -183,7 +183,7 @@
    1.22            in
    1.23              take_time timeout (fn () => goal tac)
    1.24            end)
    1.25 -          handle ZeroTime => K (SOME Time.zeroTime)
    1.26 +          handle ZEROTIME => K (SOME Time.zeroTime)
    1.27  
    1.28        val try_metis_quietly = the_default NONE oo try oo try_metis
    1.29