# HG changeset patch
# User haftmann
# Date 1274883450 -7200
# Node ID bac3d00a910a974cb4e8d77a09025109dc0a94b9
# Parent  e0c9d3e49e15bc1dd34a336b6b06bedf9e13ea85
dropped legacy theorem bindings

diff -r e0c9d3e49e15 -r bac3d00a910a src/HOL/Nominal/nominal_induct.ML
--- 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});