changeset 57510 | 8f1dc3b2daa5 |
parent 56057 | ad6bd8030d88 |
child 58669 | 6bade3d91c49 |
--- a/src/Pure/theory.ML Fri Jul 04 17:19:03 2014 +0200 +++ b/src/Pure/theory.ML Fri Jul 04 17:41:35 2014 +0200 @@ -262,7 +262,8 @@ else if Type.raw_instance (declT, T') then error (message true "imposes additional sort constraints on the constant declaration") else if overloaded then () - else warning (message false "is strictly less general than the declared type") + else + error (message false "is strictly less general than the declared type (overloading required)") end;