changeset 1547 | 57f7af5d7564 |
parent 1515 | 76fa21f27f22 |
child 1553 | 4355eb3b7161 |
--- a/Nominal/LFex.thy Fri Mar 19 12:28:35 2010 +0100 +++ b/Nominal/LFex.thy Fri Mar 19 14:54:30 2010 +0100 @@ -8,8 +8,6 @@ ML {* val _ = cheat_fv_rsp := false *} ML {* val _ = cheat_const_rsp := false *} ML {* val _ = cheat_equivp := false *} -ML {* val _ = cheat_fv_eqvt := false *} -ML {* val _ = cheat_alpha_eqvt := false *} nominal_datatype kind = Type