equal
deleted
inserted
replaced
333 in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end; |
333 in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end; |
334 |
334 |
335 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c])); |
335 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c])); |
336 |
336 |
337 fun mk_arities (t, Ss, S) = |
337 fun mk_arities (t, Ss, S) = |
338 let val T = Type (t, ListPair.map TFree (Name.invent_global_types (length Ss), Ss)) |
338 let val T = Type (t, map TFree (Name.invent_types_global Ss)) |
339 in map (fn c => mk_of_class (T, c)) S end; |
339 in map (fn c => mk_of_class (T, c)) S end; |
340 |
340 |
341 fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c])); |
341 fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c])); |
342 |
342 |
343 fun dest_arity tm = |
343 fun dest_arity tm = |