# HG changeset patch
# User smolkas
# Date 1357760792 -3600
# Node ID af8ecf09a58c927d32031570ca73eda79b226002
# Parent  34e8e0e8663917af7a507f77b6a5af7e0341dc85
changed exception to uppercase

diff -r 34e8e0e86639 -r af8ecf09a58c src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 09 20:29:50 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 09 20:46:32 2013 +0100
@@ -126,7 +126,7 @@
           |> maps (thms_of_name ctxt)
 
       (* TODO: add "Obtain" case *)
-      exception ZeroTime
+      exception ZEROTIME
       fun try_metis timeout (succedent, step) =
         (if not preplay then K (SOME Time.zeroTime) else
           let
@@ -158,7 +158,7 @@
                 in
                   (prop, byline, true)
                 end
-              | _ => raise ZeroTime)
+              | _ => raise ZEROTIME)
             val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
             val facts =
               (case byline of
@@ -183,7 +183,7 @@
           in
             take_time timeout (fn () => goal tac)
           end)
-          handle ZeroTime => K (SOME Time.zeroTime)
+          handle ZEROTIME => K (SOME Time.zeroTime)
 
       val try_metis_quietly = the_default NONE oo try oo try_metis