src/Pure/type.ML

     log_types: string list}
   val empty_tsig: tsig
   val class_space: tsig -> Name_Space.T
   val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
   val intern_class: tsig -> xstring -> string
-  val extern_class: tsig -> string -> xstring
+  val extern_class: Proof.context -> tsig -> string -> xstring
   val defaultS: tsig -> sort
   val logical_types: tsig -> string list
   val eq_sort: tsig -> sort * sort -> bool
   val subsort: tsig -> sort * sort -> bool
   val of_sort: tsig -> typ * sort -> bool

   val set_mode: mode -> Proof.context -> Proof.context
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val type_space: tsig -> Name_Space.T
   val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
   val intern_type: tsig -> xstring -> string
-  val extern_type: tsig -> string -> xstring
+  val extern_type: Proof.context -> tsig -> string -> xstring
   val is_logtype: tsig -> string -> bool
   val the_decl: tsig -> string -> decl
   val cert_typ_mode: mode -> tsig -> typ -> typ
   val cert_typ: tsig -> typ -> typ
   val arity_number: tsig -> string -> int

 
 fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) =>
   ((Name_Space.alias naming binding name space, classes), default, types));
 
 val intern_class = Name_Space.intern o class_space;
-val extern_class = Name_Space.extern o class_space;
+fun extern_class ctxt = Name_Space.extern ctxt o class_space;
 
 fun defaultS (TSig {default, ...}) = default;
 fun logical_types (TSig {log_types, ...}) = log_types;
 
 fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes);

 
 fun type_alias naming binding name = map_tsig (fn (classes, default, (space, types)) =>
   (classes, default, (Name_Space.alias naming binding name space, types)));
 
 val intern_type = Name_Space.intern o type_space;
-val extern_type = Name_Space.extern o type_space;
+fun extern_type ctxt = Name_Space.extern ctxt o type_space;
 
 val is_logtype = member (op =) o logical_types;
 
 
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;