equal
deleted
inserted
replaced
16 |
16 |
17 |
17 |
18 (* misc utils *) |
18 (* misc utils *) |
19 |
19 |
20 fun change_arrow 0 T = T |
20 fun change_arrow 0 T = T |
21 | change_arrow n (Type (_, [S, T])) = Type ("fun", [S, change_arrow (n - 1) T]) |
21 | change_arrow n (Type (_, [S, T])) = \<^Type>\<open>fun S \<open>change_arrow (n - 1) T\<close>\<close> |
22 | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []) |
22 | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []) |
23 |
23 |
24 fun trans_rules name2 name1 n mx = |
24 fun trans_rules name2 name1 n mx = |
25 let |
25 let |
26 val vnames = Name.invent Name.context "a" n |
26 val vnames = Name.invent Name.context "a" n |