diff -r a8c8008a2c9d -r 1e05ea0a5cd7 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Mar 03 20:45:48 2010 +0100
+++ b/src/Pure/consts.ML	Wed Mar 03 22:50:35 2010 +0100
@@ -21,8 +21,9 @@
   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
@@ -126,10 +127,15 @@
 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 *)