diff -r 2b367c80c0d7 -r 5ab97f43ec24 Nominal/ExPS6.thy
--- a/Nominal/ExPS6.thy	Tue Mar 23 09:21:43 2010 +0100
+++ b/Nominal/ExPS6.thy	Tue Mar 23 09:34:32 2010 +0100
@@ -6,6 +6,9 @@
 
 atom_decl name
 
+(* The binding structure is too complicated, so we cannot show equivalence *)
+ML {* val _ = cheat_equivp := true *}
+
 ML {* val _ = recursive := false  *}
 nominal_datatype exp6 =
   EVar name
@@ -28,6 +31,7 @@
 thm exp6_pat6.perm
 thm exp6_pat6.induct
 thm exp6_pat6.distinct
+thm exp6_pat6.supp
 
 end