equal
deleted
inserted
replaced
118 | _ => extern consts c); |
118 | _ => extern consts c); |
119 |
119 |
120 fun syntax consts (c, mx) = |
120 fun syntax consts (c, mx) = |
121 let |
121 let |
122 val ((T, _), early) = the_const consts c handle TYPE (msg, _, _) => error msg; |
122 val ((T, _), early) = the_const consts c handle TYPE (msg, _, _) => error msg; |
123 val c' = if early then NameSpace.base c else #1 (Syntax.mixfix_const c mx); |
123 val c' = if early then NameSpace.base c else Syntax.constN ^ c; |
124 in (c', T, mx) end; |
124 in (c', T, mx) end; |
125 |
125 |
126 |
126 |
127 (* read_const *) |
127 (* read_const *) |
128 |
128 |