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