correctly handle exceptions arising from (experimental) Isar proof code

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Wed Jan 29 20:11:38 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Wed Jan 29 22:34:34 2014 +0100
@@ -122,9 +122,7 @@
     fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
 
     fun of_indent ind = replicate_string (ind * indent_size) " "
-
     fun of_moreover ind = of_indent ind ^ "moreover\n"
-
     fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
 
     fun of_obtain qs nr =
@@ -136,7 +134,6 @@
          "") ^ "obtain"
 
     fun of_show_have qs = if member (op =) qs Show then "show" else "have"
-
     fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
 
     fun of_have qs nr =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jan 29 20:11:38 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jan 29 22:34:34 2014 +0100
@@ -799,8 +799,8 @@
                       |> introduce_spass_skolem
                       |> factify_atp_proof fact_names hyp_ts concl_t
                   in
-                    (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout,
-                     isar_compress, isar_try0, atp_proof, goal)
+                    (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress,
+                     isar_try0, atp_proof, goal)
                   end
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
@@ -808,7 +808,7 @@
                    subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
-                proof_text ctxt isar_proofs isar_params num_chained one_line_params
+                proof_text ctxt debug isar_proofs isar_params num_chained one_line_params
               end,
            (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
            (if important_message <> "" then

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 29 20:11:38 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 29 22:34:34 2014 +0100
@@ -14,10 +14,9 @@
   type one_line_params = Sledgehammer_Reconstructor.one_line_params
 
   type isar_params =
-    bool * bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
+    bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
 
-  val isar_proof_text : Proof.context -> bool option -> isar_params -> one_line_params -> string
-  val proof_text : Proof.context -> bool option -> (unit -> isar_params) -> int ->
+  val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
     one_line_params -> string
 end;
 
@@ -192,7 +191,7 @@
   end
 
 type isar_params =
-  bool * bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
+  bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
 
 val arith_methodss =
   [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
@@ -205,29 +204,29 @@
   [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
 val skolem_methodss = [[Metis_Method, Blast_Method], [Metis_New_Skolem_Method], [Meson_Method]]
 
-fun isar_proof_text ctxt isar_proofs
-    (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress, isar_try0,
-     atp_proof, goal)
+fun isar_proof_text ctxt debug isar_proofs isar_params
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
-    val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
-    val (_, ctxt) =
-      params
-      |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
-      |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
-    val one_line_proof = one_line_proof_text 0 one_line_params
-
-    val do_preplay = preplay_timeout <> Time.zeroTime
-    val isar_try0 = isar_try0 andalso do_preplay
-
-    val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
-    fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
-
-    fun get_role keep_role ((num, _), role, t, rule, _) =
-      if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
-
     fun isar_proof_of () =
       let
+        val SOME (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress,
+          isar_try0, atp_proof, goal) = try isar_params ()
+
+        val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
+        val (_, ctxt) =
+          params
+          |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
+          |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
+
+        val do_preplay = preplay_timeout <> Time.zeroTime
+        val isar_try0 = isar_try0 andalso do_preplay
+
+        val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
+        fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
+
+        fun get_role keep_role ((num, _), role, t, rule, _) =
+          if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
+
         val atp_proof =
           atp_proof
           |> rpair [] |-> fold_rev add_line_pass1
@@ -398,6 +397,7 @@
           end)
       end
 
+    val one_line_proof = one_line_proof_text 0 one_line_params
     val isar_proof =
       if debug then
         isar_proof_of ()
@@ -415,11 +415,11 @@
   | Play_Failed => true
   | Not_Played => false)
 
-fun proof_text ctxt isar_proofs isar_params num_chained
+fun proof_text ctxt debug isar_proofs isar_params num_chained
                (one_line_params as (preplay, _, _, _, _, _)) =
   (if isar_proofs = SOME true orelse
       (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
-     isar_proof_text ctxt isar_proofs (isar_params ())
+     isar_proof_text ctxt debug isar_proofs isar_params
    else
      one_line_proof_text num_chained) one_line_params