equal
deleted
inserted
replaced
76 |
76 |
77 fun norm thy (c, insts) = |
77 fun norm thy (c, insts) = |
78 let |
78 let |
79 fun disciplined class [ty as Type (tyco, _)] = |
79 fun disciplined class [ty as Type (tyco, _)] = |
80 let |
80 let |
81 val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]; |
81 val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class] |
|
82 handle CLASS_ERROR => error ("No such instance: " ^ tyco ^ " :: " ^ class |
|
83 ^ ",\nrequired for overloaded constant " ^ c); |
82 val vs = Name.invents Name.context "'a" (length sorts); |
84 val vs = Name.invents Name.context "'a" (length sorts); |
83 in |
85 in |
84 (c, [Type (tyco, map (fn v => TVar ((v, 0), [])) vs)]) |
86 (c, [Type (tyco, map (fn v => TVar ((v, 0), [])) vs)]) |
85 end |
87 end |
86 | disciplined class _ = |
88 | disciplined class _ = |