diff -r 0be098c61d00 -r 4bc9278a808d Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Wed Mar 03 10:39:43 2010 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Wed Mar 03 11:42:15 2010 +0100
@@ -239,7 +239,8 @@
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  permute_eqvt supp_eqvt fresh_eqvt
+  (*permute_eqvt commented out since it loops *)
+  supp_eqvt fresh_eqvt
   permute_pure
 
   (* datatypes *)