--- a/src/Pure/Isar/class.ML Wed Jan 02 15:14:25 2008 +0100
+++ b/src/Pure/Isar/class.ML Wed Jan 02 15:14:26 2008 +0100
@@ -820,6 +820,11 @@
(Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort)
then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
tycos;
+ (*this checkpoint should move to AxClass as soon as "attach" has disappeared*)
+ val _ = case map (fst o snd) params
+ of [] => ()
+ | cs => Output.legacy_feature
+ ("Missing definitions for overloaded parameters " ^ commas_quote cs)
in lthy end;
fun pretty_instantiation lthy =