changeset 1561 | c3dca6e600c8 |
parent 1553 | 4355eb3b7161 |
child 1576 | 7b8f570b2450 |
--- a/Nominal/LFex.thy Sat Mar 20 08:56:07 2010 +0100 +++ b/Nominal/LFex.thy Sat Mar 20 09:27:28 2010 +0100 @@ -6,7 +6,7 @@ atom_decl ident ML {* val _ = cheat_fv_rsp := false *} -ML {* val _ = cheat_const_rsp := false *} +ML {* val _ = cheat_alpha_bn_rsp := false *} ML {* val _ = cheat_equivp := false *} nominal_datatype kind =