src/Pure/type.ML
changeset 24484 013b98b57b86
parent 24274 cb9236269af1
child 24848 5dbbd33c3236
     1.1 --- a/src/Pure/type.ML	Thu Aug 30 15:04:41 2007 +0200
     1.2 +++ b/src/Pure/type.ML	Thu Aug 30 15:04:42 2007 +0200
     1.3 @@ -35,6 +35,9 @@
     1.4    val mode_default: mode
     1.5    val mode_syntax: mode
     1.6    val mode_abbrev: mode
     1.7 +  val get_mode: Proof.context -> mode
     1.8 +  val set_mode: mode -> Proof.context -> Proof.context
     1.9 +  val restore_mode: Proof.context -> Proof.context -> Proof.context
    1.10    val cert_typ_mode: mode -> tsig -> typ -> typ
    1.11    val cert_typ: tsig -> typ -> typ
    1.12    val arity_number: tsig -> string -> int
    1.13 @@ -155,6 +158,16 @@
    1.14  val mode_syntax = Mode {normalize = true, logical = false};
    1.15  val mode_abbrev = Mode {normalize = false, logical = false};
    1.16  
    1.17 +structure Mode = ProofDataFun
    1.18 +(
    1.19 +  type T = mode;
    1.20 +  fun init _ = mode_default;
    1.21 +);
    1.22 +
    1.23 +val get_mode = Mode.get;
    1.24 +fun set_mode mode = Mode.map (K mode);
    1.25 +fun restore_mode ctxt = set_mode (get_mode ctxt);
    1.26 +
    1.27  
    1.28  (* certified types *)
    1.29