src/Pure/Isar/proof_context.ML
changeset 61261 ddb2da7cb2e4
parent 61168 dcdfb6355a05
child 61262 7bd1eb4b056e
--- 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;