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);