--- a/src/Pure/type.ML Thu Aug 30 15:04:41 2007 +0200
+++ b/src/Pure/type.ML Thu Aug 30 15:04:42 2007 +0200
@@ -35,6 +35,9 @@
val mode_default: mode
val mode_syntax: mode
val mode_abbrev: mode
+ val get_mode: Proof.context -> mode
+ val set_mode: mode -> Proof.context -> Proof.context
+ val restore_mode: Proof.context -> Proof.context -> Proof.context
val cert_typ_mode: mode -> tsig -> typ -> typ
val cert_typ: tsig -> typ -> typ
val arity_number: tsig -> string -> int
@@ -155,6 +158,16 @@
val mode_syntax = Mode {normalize = true, logical = false};
val mode_abbrev = Mode {normalize = false, logical = false};
+structure Mode = ProofDataFun
+(
+ type T = mode;
+ fun init _ = mode_default;
+);
+
+val get_mode = Mode.get;
+fun set_mode mode = Mode.map (K mode);
+fun restore_mode ctxt = set_mode (get_mode ctxt);
+
(* certified types *)