src/Pure/Isar/toplevel.ML

   val proof: (Proof.state -> Proof.state) -> transition -> transition
   val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
   val skip_proof: (int -> int) -> transition -> transition
   val skip_proof_to_theory: (int -> bool) -> transition -> transition
   val exec_id: Document_ID.exec -> transition -> transition
-  val unknown_theory: transition -> transition
-  val unknown_context: transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val add_hook: (transition -> state -> state -> unit) -> unit
   val get_timing: transition -> Time.time option
   val put_timing: Time.time option -> transition -> transition
   val transition: bool -> transition -> state -> state * (exn * string) option

 fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
 fun is_ignored tr = name_of tr = "<ignored>";
 
 fun malformed pos msg =
   empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
-
-val unknown_theory = imperative (fn () => warning "Unknown theory context");
-val unknown_context = imperative (fn () => warning "Unknown context");
 
 
 (* theory transitions *)
 
 fun generic_theory f = transaction (fn _ =>