diff -r b4e330083383 -r 9cec4269b7f9 Nominal/ExPS6.thy
--- a/Nominal/ExPS6.thy	Fri Mar 26 10:35:26 2010 +0100
+++ b/Nominal/ExPS6.thy	Fri Mar 26 10:55:13 2010 +0100
@@ -6,7 +6,8 @@
 
 atom_decl name
 
-(* The binding structure is too complicated, so we cannot show equivalence *)
+(* 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  *}