--- a/Nominal/Ex/Classical.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/Classical.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -7,8 +7,6 @@
 atom_decl name
 atom_decl coname
 
-declare [[STEPS = 21]]
-
 nominal_datatype trm =
    Ax "name" "coname"
 |  Cut n::"coname" t1::"trm" c::"coname" t2::"trm"             bind n in t1, bind c in t2
@@ -18,15 +16,15 @@
 |  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       bind c in t1, bind n in t2
 |  ImpR c::"coname" n::"name" t::"trm" "coname"                bind n c in t
 
-thm distinct
-thm induct
-thm exhaust
-thm fv_defs
-thm bn_defs
-thm perm_simps
-thm eq_iff
-thm fv_bn_eqvt
-thm size_eqvt
+thm trm.distinct
+thm trm.induct
+thm trm.exhaust
+thm trm.fv_defs
+thm trm.bn_defs
+thm trm.perm_simps
+thm trm.eq_iff
+thm trm.fv_bn_eqvt
+thm trm.size_eqvt