equal
deleted
inserted
replaced
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 |