diff -r 01265301db7f -r dd0c569fa43d src/Pure/context.ML
--- a/src/Pure/context.ML	Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/context.ML	Sat Jan 14 17:14:06 2006 +0100
@@ -66,7 +66,6 @@
   val setup: unit -> (theory -> theory) list
   (*proof context*)
   type proof
-  exception PROOF of string * proof
   val theory_of_proof: proof -> theory
   val transfer_proof: theory -> proof -> proof
   val init_proof: theory -> proof
@@ -475,7 +474,7 @@
 
 (* use ML text *)
 
-val ml_output = (writeln, error_msg);
+val ml_output = (writeln, Output.error_msg);
 
 fun use_output verbose txt = use_text ml_output verbose (Symbol.escape txt);
 
@@ -505,15 +504,13 @@
 
 datatype proof = Proof of theory_ref * Object.T Inttab.table;
 
-exception PROOF of string * proof;
-
 fun theory_of_proof (Proof (thy_ref, _)) = deref thy_ref;
 fun data_of_proof (Proof (_, data)) = data;
 fun map_prf f (Proof (thy_ref, data)) = Proof (thy_ref, f data);
 
 fun transfer_proof thy' (prf as Proof (thy_ref, data)) =
   if not (subthy (deref thy_ref, thy')) then
-    raise PROOF ("transfer proof context: no a super theory", prf)
+    error "transfer proof context: no a super theory"
   else Proof (self_ref thy', data);