# HG changeset patch
# User wenzelm
# Date 965321015 -7200
# Node ID c30f6d0f81d22400619ba253f7843e3e58e49163
# Parent  bb029080ff8b72489948e6a5f3f3819876a11868
added unknown_theory/proof/context;

diff -r bb029080ff8b -r c30f6d0f81d2 src/Pure/Isar/toplevel.ML
--- 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 **)