added get_st;
authorwenzelm
Sat Jun 05 20:32:49 1999 +0200 (1999-06-05 ago)
changeset 67886eaf6856ee4a
parent 6787 25265c6807c3
child 6789 0e5a965de17a
added get_st;
src/Pure/Isar/proof_data.ML
     1.1 --- a/src/Pure/Isar/proof_data.ML	Sat Jun 05 20:32:10 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_data.ML	Sat Jun 05 20:32:49 1999 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4    val print: Proof.context -> unit
     1.5    val get: Proof.context -> T
     1.6    val put: T -> Proof.context -> Proof.context
     1.7 +  val get_st: Proof.state -> T
     1.8    val put_st: T -> Proof.state -> Proof.state
     1.9  end;
    1.10  
    1.11 @@ -39,6 +40,7 @@
    1.12  val print = ProofContext.print_data kind;
    1.13  val get = ProofContext.get_data kind (fn Data x => x);
    1.14  val put = ProofContext.put_data kind Data;
    1.15 +val get_st = get o Proof.context_of;
    1.16  val put_st = Proof.put_data kind Data;
    1.17  
    1.18  end;