src/Pure/consts.ML

   val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   val the_constraint: T -> string -> typ                       (*exception TYPE*)
   val space_of: T -> Name_Space.T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
+  val extern: T -> string -> xstring
   val intern_syntax: T -> xstring -> string
-  val extern: T -> string -> xstring
+  val extern_syntax: T -> string -> xstring
   val read_const: T -> string -> term
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
   val declare: Name_Space.naming -> binding * typ -> T -> T

 val is_concealed = Name_Space.is_concealed o space_of;
 
 val intern = Name_Space.intern o space_of;
 val extern = Name_Space.extern o space_of;
 
-fun intern_syntax consts name =
-  (case try Syntax.unmark_const name of
+fun intern_syntax consts s =
+  (case try Syntax.unmark_const s of
     SOME c => c
-  | NONE => intern consts name);
+  | NONE => intern consts s);
+
+fun extern_syntax consts s =
+  (case try Syntax.unmark_const s of
+    SOME c => extern consts c
+  | NONE => s);
 
 
 (* read_const *)
 
 fun read_const consts raw_c =