explicit error message for `improper` instances lacking explicit instance parameter constants
authorhaftmann
Wed, 04 Mar 2009 10:52:47 +0100
changeset 30243 09d5944e224e
parent 30228 2aaf339fb7c1
child 30244 48543b307e99
explicit error message for `improper` instances lacking explicit instance parameter constants
src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Mar 03 19:21:10 2009 +0100
+++ b/src/Pure/axclass.ML	Wed Mar 04 10:52:47 2009 +0100
@@ -234,7 +234,10 @@
 val map_inst_params = AxClassData.map o apsnd o apsnd;
 
 fun get_inst_param thy (c, tyco) =
-  (the o Symtab.lookup ((the o Symtab.lookup (fst (get_inst_params thy))) c)) tyco;
+  case Symtab.lookup ((the_default Symtab.empty o Symtab.lookup (fst (get_inst_params thy))) c) tyco
+   of SOME c' => c'
+    | NONE => error ("No instance parameter for constant " ^ quote c
+        ^ " on type constructor " ^ quote tyco);
 
 fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
       o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))