--- a/src/HOL/Nominal/nominal_induct.ML Wed May 26 16:05:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Wed May 26 16:17:30 2010 +0200
@@ -23,7 +23,7 @@
val split_all_tuples =
Simplifier.full_simplify (HOL_basic_ss addsimps
- [split_conv, split_paired_all, unit_all_eq1, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
+ [@{thm split_conv}, @{thm split_paired_all}, @{thm unit_all_eq1}, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
@{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim});