# HG changeset patch
# User haftmann
# Date 1236160367 -3600
# Node ID 09d5944e224e969091b49d04bb5bc724971bb784
# Parent  2aaf339fb7c16b4993f766169114c0f8f77a0e50
explicit error message for `improper` instances lacking explicit instance parameter constants

diff -r 2aaf339fb7c1 -r 09d5944e224e 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))