equal
deleted
inserted
replaced
101 |
101 |
102 (* arities as terms *) |
102 (* arities as terms *) |
103 |
103 |
104 fun mk_arity (t, ss, c) = |
104 fun mk_arity (t, ss, c) = |
105 let |
105 let |
106 val names = tl (variantlist (replicate (length ss + 1) "'", [])); |
106 val tfrees = ListPair.map TFree (Term.invent_names (length ss + 1) "'", ss); |
107 val tfrees = ListPair.map TFree (names, ss); |
|
108 in Logic.mk_inclass (Type (t, tfrees), c) end; |
107 in Logic.mk_inclass (Type (t, tfrees), c) end; |
109 |
108 |
110 fun dest_arity tm = |
109 fun dest_arity tm = |
111 let |
110 let |
112 fun err () = raise TERM ("dest_arity", [tm]); |
111 fun err () = raise TERM ("dest_arity", [tm]); |