--- a/Nominal/Ex/Modules.thy	Mon Sep 20 21:52:45 2010 +0800
+++ b/Nominal/Ex/Modules.thy	Wed Sep 22 14:19:48 2010 +0800
@@ -2,14 +2,14 @@
 imports "../Nominal2"
 begin
 
-(* example from Leroy'96 about modules; 
-   see OTT example by Owens *)
+(* 
+   example from Leroy'96 about modules
+
+   see OTT example by Owens 
+*)
 
 atom_decl name
 
-declare [[STEPS = 31]]
-
-
 nominal_datatype modules: 
  mexp =
   Acc "path"
@@ -72,7 +72,7 @@
 thm modules.eq_iff
 thm modules.fv_bn_eqvt
 thm modules.size_eqvt
-
+thm modules.supp
 
 
 end