more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);

--- a/src/HOL/Library/refute.ML	Wed Mar 27 17:55:21 2013 +0100
+++ b/src/HOL/Library/refute.ML	Wed Mar 27 17:58:07 2013 +0100
@@ -3202,6 +3202,7 @@
     "try to find a model that refutes a given subgoal"
     (scan_parms -- Scan.optional Parse.nat 1 >>
       (fn (parms, i) =>
+        Toplevel.unknown_proof o
         Toplevel.keep (fn state =>
           let
             val ctxt = Toplevel.context_of state;

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Mar 27 17:55:21 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Mar 27 17:58:07 2013 +0100
@@ -368,11 +368,6 @@
   in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end
   |> `(fn (outcome_code, _) => outcome_code = genuineN)
 
-fun nitpick_trans (params, i) =
-  Toplevel.keep (fn state =>
-      pick_nits params Normal i (Toplevel.proof_position_of state)
-                (Toplevel.proof_of state) |> K ())
-
 fun string_for_raw_param (name, value) =
   name ^ " = " ^ stringify_raw_param_value value
 
@@ -391,7 +386,11 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "nitpick"}
     "try to find a counterexample for a given subgoal using Nitpick"
-    ((parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans)
+    (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
+      Toplevel.unknown_proof o
+      Toplevel.keep (fn state =>
+        ignore (pick_nits params Normal i (Toplevel.proof_position_of state)
+          (Toplevel.proof_of state)))))
 
 val _ =
   Outer_Syntax.command @{command_spec "nitpick_params"}

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Mar 27 17:55:21 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Mar 27 17:58:07 2013 +0100
@@ -419,6 +419,7 @@
   end
 
 fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
+  Toplevel.unknown_proof o
   Toplevel.keep (hammer_away params subcommand opt_i fact_override
                  o Toplevel.proof_of)
 

--- a/src/HOL/Tools/try0.ML	Wed Mar 27 17:55:21 2013 +0100
+++ b/src/HOL/Tools/try0.ML	Wed Mar 27 17:58:07 2013 +0100
@@ -156,6 +156,7 @@
 fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt
 
 fun try0_trans quad =
+  Toplevel.unknown_proof o
   Toplevel.keep (K () o do_try0 Normal (SOME default_timeout) quad
                  o Toplevel.proof_of)
 

--- a/src/Tools/quickcheck.ML	Wed Mar 27 17:55:21 2013 +0100
+++ b/src/Tools/quickcheck.ML	Wed Mar 27 17:58:07 2013 +0100
@@ -532,8 +532,8 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "quickcheck"}
     "try to find counterexample for subgoal"
-    (parse_args -- Scan.optional Parse.nat 1
-      >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
+    (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
+      Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
 
 
 (* automatic testing *)

--- a/src/Tools/solve_direct.ML	Wed Mar 27 17:55:21 2013 +0100
+++ b/src/Tools/solve_direct.ML	Wed Mar 27 17:58:07 2013 +0100
@@ -109,7 +109,8 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "solve_direct"}
     "try to solve conjectures directly with existing theorems"
-    (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
+    (Scan.succeed (Toplevel.unknown_proof o
+      Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
 
 
 (* hook *)

--- a/src/Tools/try.ML	Wed Mar 27 17:55:21 2013 +0100
+++ b/src/Tools/try.ML	Wed Mar 27 17:58:07 2013 +0100
@@ -90,7 +90,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "try"}
     "try a combination of automatic proving and disproving tools"
-    (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
+    (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
 
 
 (* automatic try *)