equal
deleted
inserted
replaced
260 in |
260 in |
261 if Sign.typ_instance thy (declT, T') then () |
261 if Sign.typ_instance thy (declT, T') then () |
262 else if Type.raw_instance (declT, T') then |
262 else if Type.raw_instance (declT, T') then |
263 error (message true "imposes additional sort constraints on the constant declaration") |
263 error (message true "imposes additional sort constraints on the constant declaration") |
264 else if overloaded then () |
264 else if overloaded then () |
265 else warning (message false "is strictly less general than the declared type") |
265 else |
|
266 error (message false "is strictly less general than the declared type (overloading required)") |
266 end; |
267 end; |
267 |
268 |
268 |
269 |
269 (* definitional axioms *) |
270 (* definitional axioms *) |
270 |
271 |