explicit error for Toplevel.proof_of;
eliminated obsolete Toplevel.unknown_proof;
more total Toplevel.proof_position_of;

--- a/NEWS	Thu Apr 16 13:48:10 2015 +0200
+++ b/NEWS	Thu Apr 16 14:18:32 2015 +0200
@@ -398,6 +398,9 @@
 derivatives) instead, which is not affected by the change. Potential
 INCOMPATIBILITY in rare applications of Name_Space.intern.
 
+* Subtle change of error semantics of Toplevel.proof_of: regular user
+ERROR instead of internal Toplevel.UNDEF.
+
 * Basic combinators map, fold, fold_map, split_list, apply are available
 as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
 

--- a/src/Doc/Implementation/Integration.thy	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/Doc/Implementation/Integration.thy	Thu Apr 16 14:18:32 2015 +0200
@@ -62,7 +62,7 @@
   for an empty toplevel state.
 
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
-  state if available, otherwise it raises @{ML Toplevel.UNDEF}.
+  state if available, otherwise it raises an error.
 
   \end{description}
 \<close>

--- a/src/HOL/Library/refute.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/HOL/Library/refute.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -2969,7 +2969,6 @@
     "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_commands.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -377,7 +377,6 @@
   Outer_Syntax.command @{command_keyword nitpick}
     "try to find a counterexample for a given subgoal using Nitpick"
     (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)))))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -359,7 +359,6 @@
   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)
 
 fun string_of_raw_param (key, values) =

--- a/src/HOL/Tools/try0.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -154,7 +154,6 @@
 fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt;
 
 fun try0_trans quad =
-  Toplevel.unknown_proof o
   Toplevel.keep (K () o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of);
 
 fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2);

--- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -240,10 +240,7 @@
   in ML_Context.eval_source_in opt_ctxt flags source end);
 
 val diag_state = Diag_State.get;
-
-fun diag_goal ctxt =
-  Proof.goal (Toplevel.proof_of (diag_state ctxt))
-    handle Toplevel.UNDEF => error "No goal present";
+val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
 
 val _ = Theory.setup
   (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})

--- a/src/Pure/Isar/proof.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -338,7 +338,7 @@
   fun find i state =
     (case try current_goal state of
       SOME (ctxt, goal) => (ctxt, (i, goal))
-    | NONE => find (i + 1) (close_block state handle ERROR _ => error "No goal present"));
+    | NONE => find (i + 1) (close_block state handle ERROR _ => error "No proof goal"));
 in val find_goal = find 0 end;
 
 fun get_goal state =

--- a/src/Pure/Isar/toplevel.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -73,7 +73,6 @@
   val skip_proof_to_theory: (int -> bool) -> transition -> transition
   val exec_id: Document_ID.exec -> transition -> transition
   val unknown_theory: transition -> transition
-  val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val add_hook: (transition -> state -> state -> unit) -> unit
@@ -164,12 +163,12 @@
 val context_of = node_case Context.proof_of Proof.context_of;
 val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
 val theory_of = node_case Context.theory_of Proof.theory_of;
-val proof_of = node_case (fn _ => raise UNDEF) I;
+val proof_of = node_case (fn _ => error "No proof state") I;
 
 fun proof_position_of state =
   (case node_of state of
     Proof (prf, _) => Proof_Node.position prf
-  | _ => raise UNDEF);
+  | _ => ~1);
 
 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
   | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
@@ -357,7 +356,6 @@
   empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
 
 val unknown_theory = imperative (fn () => warning "Unknown theory context");
-val unknown_proof = imperative (fn () => warning "Unknown proof context");
 val unknown_context = imperative (fn () => warning "Unknown context");
 
 

--- a/src/Pure/Thy/thy_output.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -614,16 +614,12 @@
 
 local
 
-fun proof_state state =
-  (case try (Proof.goal o Toplevel.proof_of) state of
-    SOME {goal, ...} => goal
-  | _ => error "No proof state");
-
 fun goal_state name main = antiquotation name (Scan.succeed ())
   (fn {state, context = ctxt, ...} => fn () =>
     output ctxt
       [Goal_Display.pretty_goal
-        (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
+        (Config.put Goal_Display.show_main_goal main ctxt)
+        (#goal (Proof.goal (Toplevel.proof_of state)))]);
 
 in
 

--- a/src/Tools/quickcheck.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/Tools/quickcheck.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -533,8 +533,8 @@
 val _ =
   Outer_Syntax.command @{command_keyword quickcheck}
     "try to find counterexample for subgoal"
-    (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
-      Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
+    (parse_args -- Scan.optional Parse.nat 1 >>
+      (fn (args, i) => Toplevel.keep (quickcheck_cmd args i)));
 
 
 (* automatic testing *)

--- a/src/Tools/solve_direct.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/Tools/solve_direct.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -94,8 +94,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword solve_direct}
     "try to solve conjectures directly with existing theorems"
-    (Scan.succeed (Toplevel.unknown_proof o
-      Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
+    (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
 
 
 (* hook *)

--- a/src/Tools/try.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/Tools/try.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -77,7 +77,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword try}
     "try a combination of automatic proving and disproving tools"
-    (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
+    (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
 
 
 (* automatic try (TTY) *)