equal
deleted
inserted
replaced
134 (* check *) |
134 (* check *) |
135 |
135 |
136 fun bad binding = "Bad name binding: " ^ print binding ^ Position.here (pos_of binding); |
136 fun bad binding = "Bad name binding: " ^ print binding ^ Position.here (pos_of binding); |
137 |
137 |
138 fun check binding = |
138 fun check binding = |
139 if Symbol.is_ident (Symbol.explode (name_of binding)) then () |
139 if Symbol_Pos.is_identifier (name_of binding) then () |
140 else legacy_feature (bad binding); |
140 else legacy_feature (bad binding); |
141 |
141 |
142 end; |
142 end; |
143 end; |
143 end; |
144 |
144 |