# HG changeset patch
# User haftmann
# Date 1199283266 -3600
# Node ID cb11c9ee25383216282177db458206c11b013c32
# Parent  850abe253ffc3643bc6825c44219bfa4de9241d4
clarified policy

diff -r 850abe253ffc -r cb11c9ee2538 src/Pure/Isar/class.ML
--- 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 =