--- a/Nominal/TySch.thy	Tue Mar 23 08:22:48 2010 +0100
+++ b/Nominal/TySch.thy	Tue Mar 23 08:33:48 2010 +0100
@@ -4,8 +4,6 @@
 
 atom_decl name
 
-ML {* val _ = cheat_equivp := false *}
-
 nominal_datatype t =
   Var "name"
 | Fun "t" "t"