src/Pure/consts.ML

--- a/src/Pure/consts.ML	Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/consts.ML	Fri Apr 08 16:34:14 2011 +0200
@@ -132,12 +132,12 @@
 val extern = Name_Space.extern o space_of;
 
 fun intern_syntax consts s =
-  (case try Syntax.unmark_const s of
+  (case try Lexicon.unmark_const s of
     SOME c => c
   | NONE => intern consts s);
 
 fun extern_syntax consts s =
-  (case try Syntax.unmark_const s of
+  (case try Lexicon.unmark_const s of
     SOME c => extern consts c
   | NONE => s);