--- a/src/Pure/defs.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/defs.ML Fri Sep 25 19:13:47 2015 +0200
@@ -13,6 +13,7 @@
val item_kind_ord: item_kind * item_kind -> order
val plain_args: typ list -> bool
type context = Proof.context * (Name_Space.T * Name_Space.T) option
+ val global_context: theory -> context
val space: context -> item_kind -> Name_Space.T
val pretty_item: context -> item -> Pretty.T
val pretty_args: Proof.context -> typ list -> Pretty.T list
@@ -55,6 +56,8 @@
type context = Proof.context * (Name_Space.T * Name_Space.T) option;
+fun global_context thy : context = (Syntax.init_pretty_global thy, NONE);
+
fun space (ctxt, spaces) kind =
(case (kind, spaces) of
(Const, SOME (const_space, _)) => const_space