equal
deleted
inserted
replaced
78 (* arities as terms *) |
78 (* arities as terms *) |
79 |
79 |
80 fun mk_arity (t, ss, c) = |
80 fun mk_arity (t, ss, c) = |
81 let |
81 let |
82 val names = tl (variantlist (replicate (length ss + 1) "'", [])); |
82 val names = tl (variantlist (replicate (length ss + 1) "'", [])); |
83 val tfrees = map TFree (names ~~ ss); |
83 val tfrees = ListPair.map TFree (names, ss); |
84 in |
84 in |
85 Logic.mk_inclass (Type (t, tfrees), c) |
85 Logic.mk_inclass (Type (t, tfrees), c) |
86 end; |
86 end; |
87 |
87 |
88 fun dest_arity tm = |
88 fun dest_arity tm = |