changeset 19673 | 853f5a3cc06e |
parent 19657 | 25eaa3660123 |
child 19677 | 9d54d6d3bc28 |
--- a/src/Pure/consts.ML Wed May 17 01:23:44 2006 +0200 +++ b/src/Pure/consts.ML Wed May 17 01:23:46 2006 +0200 @@ -120,7 +120,7 @@ fun syntax consts (c, mx) = let val ((T, _), early) = the_const consts c handle TYPE (msg, _, _) => error msg; - val c' = if early then NameSpace.base c else #1 (Syntax.mixfix_const c mx); + val c' = if early then NameSpace.base c else Syntax.constN ^ c; in (c', T, mx) end;