--- a/src/Pure/Isar/toplevel.ML Thu Aug 03 11:51:11 2000 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Aug 03 18:43:35 2000 +0200
@@ -53,6 +53,9 @@
val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
+ val unknown_theory: transition -> transition
+ val unknown_proof: transition -> transition
+ val unknown_context: transition -> transition
val quiet: bool ref
val exn_message: exn -> string
val apply: bool -> transition -> state -> (state * (exn * string) option) option
@@ -347,6 +350,10 @@
val proof = proof' o K;
fun proof_to_theory f = map_current (fn _ => (fn Proof prf => Theory (f prf) | _ => raise UNDEF));
+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");
+
(** toplevel transactions **)