# HG changeset patch
# User haftmann
# Date 1172910421 -3600
# Node ID cb0b1bbf7e910275f08356dff24a22b5a53ed862
# Parent  80395c2c40cca291c5db74a0d3a292e62f419f59
clarified error message

diff -r 80395c2c40cc -r cb0b1bbf7e91 src/Pure/Tools/codegen_consts.ML
--- a/src/Pure/Tools/codegen_consts.ML	Sat Mar 03 09:27:00 2007 +0100
+++ b/src/Pure/Tools/codegen_consts.ML	Sat Mar 03 09:27:01 2007 +0100
@@ -78,7 +78,9 @@
   let
     fun disciplined class [ty as Type (tyco, _)] =
           let
-            val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
+            val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]
+              handle CLASS_ERROR => error ("No such instance: " ^ tyco ^ " :: " ^ class
+                ^ ",\nrequired for overloaded constant " ^ c);
             val vs = Name.invents Name.context "'a" (length sorts);
           in
             (c, [Type (tyco, map (fn v => TVar ((v, 0), [])) vs)])