clarified error message
authorhaftmann
Sat, 03 Mar 2007 09:27:01 +0100
changeset 22400 cb0b1bbf7e91
parent 22399 80395c2c40cc
child 22401 51997956e7d1
clarified error message
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)])