diff -r a5dc3558cdec -r 3b83960f9544 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Thu May 20 21:23:53 2010 +0100
@@ -4,6 +4,9 @@
 
 atom_decl name
 
+ML {* print_depth 50 *}
+declare [[STEPS = 19]]
+
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
@@ -16,6 +19,8 @@
 where
   "bn (As x t) = {atom x}"
 
+thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars]
+
 ML {* Inductive.the_inductive *}
 thm trm_assg.fv
 thm trm_assg.supp
@@ -26,8 +31,10 @@
 thm trm_assg.inducts
 thm trm_assg.distinct
 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
+
+(* TEMPORARY
 thm trm_assg.fv[simplified trm_assg.supp(1-2)]
-
+*)