diff -r 8f8652a8107f -r 2f289c1f6cf1 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Sat Sep 11 05:56:49 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Sep 12 22:46:40 2010 +0800
@@ -2,6 +2,11 @@
 imports "../Nominal2" 
 begin
 
+ML {*
+Inductive.unpartition_rules
+*}
+
+
 atom_decl name
 
 declare [[STEPS = 100]]