# HG changeset patch
# User haftmann
# Date 1236163070 -3600
# Node ID 48543b307e99a2496b9ae5e7e7bfd64f162c5235
# Parent  aea5d7fa7ef5c14c4caf42ba85c4682d90484755# Parent  09d5944e224e969091b49d04bb5bc724971bb784
merged

diff -r aea5d7fa7ef5 -r 48543b307e99 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Mar 04 11:05:29 2009 +0100
+++ b/src/Pure/axclass.ML	Wed Mar 04 11:37:50 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))