diff -r 29532d69111c -r b51532dd5689 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Fri Jun 18 15:22:58 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Wed Jun 23 08:48:38 2010 +0200
@@ -4,6 +4,8 @@
 
 atom_decl name
 
+ML {* val _ = cheat_equivp := true *}
+
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
@@ -27,7 +29,7 @@
 thm trm_assg.inducts
 thm trm_assg.distinct
 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
-thm trm_assg.fv[simplified trm_assg.supp(1-2)]
+(* thm trm_assg.fv[simplified trm_assg.supp(1-2)] *)
 
 
 end