diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Apr 16 13:48:45 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 16 15:25:25 2011 +0200
@@ -37,6 +37,15 @@
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
   val facts_of: Proof.context -> Facts.T
   val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
+  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 intern_class: Proof.context -> xstring -> string
+  val intern_type: Proof.context -> xstring -> string
+  val intern_const: Proof.context -> xstring -> string
+  val extern_class: Proof.context -> string -> xstring
+  val extern_type: Proof.context -> string -> xstring
+  val extern_const: Proof.context -> string -> xstring
   val transfer_syntax: theory -> Proof.context -> Proof.context
   val transfer: theory -> Proof.context -> Proof.context
   val background_theory: (theory -> theory) -> Proof.context -> Proof.context
@@ -269,6 +278,21 @@
 val cases_of = #cases o rep_context;
 
 
+(* name spaces *)
+
+val class_space = Type.class_space o tsig_of;
+val type_space = Type.type_space o tsig_of;
+val const_space = Consts.space_of o consts_of;
+
+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;
+
+fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt);
+fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt);
+fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt);
+
+
 (* theory transfer *)
 
 fun transfer_syntax thy ctxt = ctxt |>
@@ -351,7 +375,7 @@
 
 in
 
-val read_arity = prep_arity (Type.intern_type o tsig_of) Syntax.read_sort;
+val read_arity = prep_arity intern_type Syntax.read_sort;
 val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
 
 end;
@@ -452,7 +476,7 @@
       TFree (c, default_sort ctxt (c, ~1)))
     else
       let
-        val d = Type.intern_type tsig c;
+        val d = intern_type ctxt c;
         val decl = Type.the_decl tsig d;
         val _ = Context_Position.report ctxt pos (Markup.tycon d);
         fun err () = error ("Bad type name: " ^ quote d);