--- a/Nominal/ExPS6.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/ExPS6.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -8,7 +8,6 @@
 
 (* The binding structure is too complicated, so equivalence the
    way we define it is not true *)
-ML {* val _ = cheat_equivp := true *}
 
 ML {* val _ = recursive := false  *}
 nominal_datatype exp6 =