diff -r ac69ed8303cc -r 304bd7400a47 Nominal/ExPS6.thy
--- a/Nominal/ExPS6.thy	Tue Mar 23 10:24:12 2010 +0100
+++ b/Nominal/ExPS6.thy	Tue Mar 23 10:26:46 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