src/Pure/type.ML

--- a/src/Pure/type.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/type.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -28,7 +28,7 @@
   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
@@ -49,7 +49,7 @@
   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
@@ -192,7 +192,7 @@
   ((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;
@@ -237,7 +237,7 @@
   (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;