--- a/src/Pure/Isar/proof_context.ML Thu Sep 24 13:33:42 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Sep 24 23:33:29 2015 +0200
@@ -44,6 +44,7 @@
val class_space: Proof.context -> Name_Space.T
val type_space: Proof.context -> Name_Space.T
val const_space: Proof.context -> Name_Space.T
+ val defs_context: Proof.context -> Defs.context
val intern_class: Proof.context -> xstring -> string
val intern_type: Proof.context -> xstring -> string
val intern_const: Proof.context -> xstring -> string
@@ -322,6 +323,8 @@
val type_space = Type.type_space o tsig_of;
val const_space = Consts.space_of o consts_of;
+fun defs_context ctxt = (ctxt, SOME (const_space ctxt, type_space ctxt));
+
val intern_class = Name_Space.intern o class_space;
val intern_type = Name_Space.intern o type_space;
val intern_const = Name_Space.intern o const_space;