--- a/Nominal/LFex.thy	Tue Mar 23 08:22:48 2010 +0100
+++ b/Nominal/LFex.thy	Tue Mar 23 08:33:48 2010 +0100
@@ -5,8 +5,6 @@
 atom_decl name
 atom_decl ident
 
-ML {* val _ = cheat_equivp := false *}
-
 nominal_datatype kind =
     Type
   | KPi "ty" n::"name" k::"kind" bind n in k