src/Pure/consts.ML
changeset 35262 9ea4445d2ccf
parent 35255 2cb27605301f
child 35554 1e05ea0a5cd7
--- a/src/Pure/consts.ML	Sun Feb 21 21:41:29 2010 +0100
+++ b/src/Pure/consts.ML	Sun Feb 21 22:35:02 2010 +0100
@@ -127,7 +127,7 @@
 val extern = Name_Space.extern o space_of;
 
 fun intern_syntax consts name =
-  (case try (unprefix Syntax.constN) name of
+  (case try Syntax.unmark_const name of
     SOME c => c
   | NONE => intern consts name);