# HG changeset patch
# User wenzelm
# Date 1026837785 -7200
# Node ID a21e132c3304d4212b54f071ce685b5344f4e889
# Parent  b261d9cdd6b2f39646863f3778b6d00cf42ff7be
rearranged to work without proof contexts;

diff -r b261d9cdd6b2 -r a21e132c3304 src/Pure/Isar/proof_data.ML
--- a/src/Pure/Isar/proof_data.ML	Tue Jul 16 18:42:07 2002 +0200
+++ b/src/Pure/Isar/proof_data.ML	Tue Jul 16 18:43:05 2002 +0200
@@ -11,20 +11,17 @@
   val name: string
   type T
   val init: theory -> T
-  val print: Proof.context -> T -> unit
+  val print: ProofContext.context -> T -> unit
 end;
 
 signature PROOF_DATA =
 sig
   type T
   val init: theory -> theory
-  val print: Proof.context -> unit
-  val get: Proof.context -> T
-  val put: T -> Proof.context -> Proof.context
-  val map: (T -> T) -> Proof.context -> Proof.context
-  val get_st: Proof.state -> T
-  val put_st: T -> Proof.state -> Proof.state
-  val map_st: (T -> T) -> Proof.state -> Proof.state
+  val print: ProofContext.context -> unit
+  val get: ProofContext.context -> T
+  val put: T -> ProofContext.context -> ProofContext.context
+  val map: (T -> T) -> ProofContext.context -> ProofContext.context
 end;
 
 functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
@@ -45,13 +42,8 @@
 val put = ProofContext.put_data kind Data;
 fun map f ctxt = put (f (get ctxt)) ctxt;
 
-val get_st = get o Proof.context_of;
-val put_st = Proof.put_data kind Data;
-fun map_st f st = put_st (f (get_st st)) st;
-
 end;
 
 
 (*hide private data access functions*)
 structure ProofContext: PROOF_CONTEXT = ProofContext;
-structure Proof: PROOF = Proof;