src/Pure/Isar/class.ML
changeset 25770 cb11c9ee2538
parent 25711 91cee0cefaf7
child 25829 4b44d945702f
     1.1 --- a/src/Pure/Isar/class.ML	Wed Jan 02 15:14:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Jan 02 15:14:26 2008 +0100
     1.3 @@ -820,6 +820,11 @@
     1.4          (Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort)
     1.5        then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
     1.6          tycos;
     1.7 +    (*this checkpoint should move to AxClass as soon as "attach" has disappeared*)
     1.8 +    val _ = case map (fst o snd) params
     1.9 +     of [] => ()
    1.10 +      | cs => Output.legacy_feature
    1.11 +          ("Missing definitions for overloaded parameters " ^ commas_quote cs)
    1.12    in lthy end;
    1.13  
    1.14  fun pretty_instantiation lthy =