src/Pure/axclass.ML
changeset 30243 09d5944e224e
parent 29579 cb520b766e00
child 30244 48543b307e99
equal deleted inserted replaced
30228:2aaf339fb7c1 30243:09d5944e224e
   232 
   232 
   233 val get_inst_params = #2 o #2 o AxClassData.get;
   233 val get_inst_params = #2 o #2 o AxClassData.get;
   234 val map_inst_params = AxClassData.map o apsnd o apsnd;
   234 val map_inst_params = AxClassData.map o apsnd o apsnd;
   235 
   235 
   236 fun get_inst_param thy (c, tyco) =
   236 fun get_inst_param thy (c, tyco) =
   237   (the o Symtab.lookup ((the o Symtab.lookup (fst (get_inst_params thy))) c)) tyco;
   237   case Symtab.lookup ((the_default Symtab.empty o Symtab.lookup (fst (get_inst_params thy))) c) tyco
       
   238    of SOME c' => c'
       
   239     | NONE => error ("No instance parameter for constant " ^ quote c
       
   240         ^ " on type constructor " ^ quote tyco);
   238 
   241 
   239 fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
   242 fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
   240       o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
   243       o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
   241   #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
   244   #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
   242 
   245