# HG changeset patch
# User wenzelm
# Date 1124192551 -7200
# Node ID cca2f393844345f1ba57c4f152f9ef462f470558
# Parent  a001a3ebfcfd9b3008d652875274adc2fb1a916c
type proof: theory_ref instead of theory (make proof contexts independent entities);
added transfer_proof;

diff -r a001a3ebfcfd -r cca2f3938443 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Aug 16 13:42:30 2005 +0200
+++ b/src/Pure/context.ML	Tue Aug 16 13:42:31 2005 +0200
@@ -67,7 +67,9 @@
   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
   val proof_data_of: theory -> string list
   (*generic context*)
@@ -472,10 +474,10 @@
 
 val ml_output = (writeln, error_msg);
 
-fun use_output verb txt = use_text ml_output verb (Symbol.escape txt);
+fun use_output verbose txt = use_text ml_output verbose (Symbol.escape txt);
 
-fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) ();
-fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt);
+fun use_mltext txt verbose opt_thy = setmp opt_thy (fn () => use_output verbose txt) ();
+fun use_mltext_theory txt verbose thy = #2 (pass_theory thy (use_output verbose) txt);
 
 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
 
@@ -498,11 +500,18 @@
 
 (* datatype proof *)
 
-datatype proof = Proof of theory * Object.T Inttab.table;
+datatype proof = Proof of theory_ref * Object.T Inttab.table;
+
+exception PROOF of string * proof;
 
-fun theory_of_proof (Proof (thy, _)) = thy;
+fun theory_of_proof (Proof (thy_ref, _)) = deref thy_ref;
 fun data_of_proof (Proof (_, data)) = data;
-fun map_prf f (Proof (thy, data)) = Proof (thy, f 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)
+  else Proof (self_ref thy', data);
 
 
 (* proof data kinds *)
@@ -529,7 +538,7 @@
 val proof_data_of = dest_data invoke_name o #proof o data_of;
 
 fun init_proof thy =
-  Proof (thy, Inttab.map' (fn k => fn _ => invoke_init k thy) (#proof (data_of thy)));
+  Proof (self_ref thy, Inttab.map' (fn k => fn _ => invoke_init k thy) (#proof (data_of thy)));
 
 structure ProofData =
 struct