merged

--- a/src/HOL/SPARK/SPARK.thy	Thu Jan 10 21:20:14 2013 +0100
+++ b/src/HOL/SPARK/SPARK.thy	Thu Jan 10 23:02:58 2013 +0100
@@ -275,4 +275,11 @@
   qed
 qed
 
+
+text {* Minimum and maximum *}
+
+spark_proof_functions
+  integer__min = "min :: int \<Rightarrow> int \<Rightarrow> int"
+  integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int"
+
 end

--- a/src/HOL/SPARK/Tools/spark_commands.ML	Thu Jan 10 21:20:14 2013 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Thu Jan 10 23:02:58 2013 +0100
@@ -75,7 +75,7 @@
     Specification.theorem Thm.theoremK NONE
       (fn thmss => (Local_Theory.background_theory
          (SPARK_VCs.mark_proved vc_name (flat thmss))))
-      (Binding.name vc_name, []) [] ctxt stmt true lthy
+      (Binding.name vc_name, []) [] ctxt stmt false lthy
   end;
 
 fun string_of_status NONE = "(unproved)"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Jan 10 21:20:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Jan 10 23:02:58 2013 +0100
@@ -69,7 +69,8 @@
     in
       fun handle_metis_fail try_metis () =
         try_metis () handle exp =>
-          (if debug then raise exp else metis_fail := true; SOME Time.zeroTime)
+          (if Exn.is_interrupt exp orelse debug then reraise exp 
+           else metis_fail := true; SOME Time.zeroTime)
       fun get_time lazy_time =
         if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
       val metis_fail = fn () => !metis_fail
@@ -125,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
@@ -157,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
@@ -182,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
 
@@ -208,11 +209,12 @@
                 (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
                   (fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
               | (Obtain(qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
-                  (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2) )
+                  (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
+              | _ => error "Internal error: unmergeable Isar steps" )
             val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
             val gfs = union (op =) gfs1 gfs2
           in step_constructor (By_Metis (lfs, gfs)) end
-        | merge _ _ = error "Internal error: Unmergeable Isar steps"
+        | merge _ _ = error "Internal error: unmergeable Isar steps"
 
       fun try_merge metis_time (s1, i) (s2, j) =
         (case get i metis_time |> Lazy.force of