equal
deleted
inserted
replaced
6 atom_decl ident |
6 atom_decl ident |
7 |
7 |
8 ML {* val _ = cheat_fv_rsp := false *} |
8 ML {* val _ = cheat_fv_rsp := false *} |
9 ML {* val _ = cheat_const_rsp := false *} |
9 ML {* val _ = cheat_const_rsp := false *} |
10 ML {* val _ = cheat_equivp := false *} |
10 ML {* val _ = cheat_equivp := false *} |
11 ML {* val _ = cheat_fv_eqvt := false *} |
|
12 ML {* val _ = cheat_alpha_eqvt := false *} |
|
13 |
11 |
14 nominal_datatype kind = |
12 nominal_datatype kind = |
15 Type |
13 Type |
16 | KPi "ty" n::"name" k::"kind" bind n in k |
14 | KPi "ty" n::"name" k::"kind" bind n in k |
17 and ty = |
15 and ty = |