src/Pure/Isar/proof_data.ML
changeset 6777 175ff298ac0e
parent 5821 262ce90e4736
child 6788 6eaf6856ee4a
     1.1 --- a/src/Pure/Isar/proof_data.ML	Fri Jun 04 19:55:11 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_data.ML	Fri Jun 04 19:55:26 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 put_st: T -> Proof.state -> Proof.state
     1.8  end;
     1.9  
    1.10  functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
    1.11 @@ -38,6 +39,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 put_st = Proof.put_data kind Data;
    1.16  
    1.17  end;
    1.18