diff -r e73bd379e839 -r e8732350a29f Nominal/nominal_induct.ML
--- a/Nominal/nominal_induct.ML	Thu Dec 30 10:00:09 2010 +0000
+++ b/Nominal/nominal_induct.ML	Fri Dec 31 12:12:59 2010 +0000
@@ -24,11 +24,10 @@
 
 val split_all_tuples =
   Simplifier.full_simplify (HOL_basic_ss addsimps
-    @{thms split_conv split_paired_all unit_all_eq1})
-(* 
-     @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
-     @{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim})
-*)
+    @{thms split_conv split_paired_all unit_all_eq1} @
+    @{thms fresh_Unit_elim fresh_Pair_elim} @
+    @{thms fresh_star_Unit_elim fresh_star_Pair_elim fresh_star_Un_elim} @
+    @{thms fresh_star_insert_elim fresh_star_empty_elim})
 
 
 (* prepare rule *)