213 |
213 |
214 |
214 |
215 (* declaration and definition of instances of overloaded constants *) |
215 (* declaration and definition of instances of overloaded constants *) |
216 |
216 |
217 fun inst_tyco_of thy (c, T) = |
217 fun inst_tyco_of thy (c, T) = |
218 (case get_inst_tyco (Sign.consts_of thy) (c, T) of |
218 get_inst_tyco (Sign.consts_of thy) (c, T) |
219 SOME tyco => tyco |
219 |> \<^if_none>\<open> |
220 | NONE => error ("Illegal type for instantiation of class parameter: " ^ |
220 error ("Illegal type for instantiation of class parameter: " ^ |
221 quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T))); |
221 quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T))\<close>; |
222 |
222 |
223 fun declare_overloaded (c, T) thy = |
223 fun declare_overloaded (c, T) thy = |
224 let |
224 let |
225 val class = |
225 val class = class_of_param thy c |> \<^if_none>\<open>error ("Not a class parameter: " ^ quote c)\<close>; |
226 (case class_of_param thy c of |
|
227 SOME class => class |
|
228 | NONE => error ("Not a class parameter: " ^ quote c)); |
|
229 val tyco = inst_tyco_of thy (c, T); |
226 val tyco = inst_tyco_of thy (c, T); |
230 val name_inst = instance_name (tyco, class) ^ "_inst"; |
227 val name_inst = instance_name (tyco, class) ^ "_inst"; |
231 val c' = instance_name (tyco, c); |
228 val c' = instance_name (tyco, c); |
232 val T' = Type.strip_sorts T; |
229 val T' = Type.strip_sorts T; |
233 in |
230 in |