diff -r d0961e6d6881 -r 5ac9a74d22fd Nominal/nominal_dt_supp.ML
--- a/Nominal/nominal_dt_supp.ML	Mon Sep 27 04:56:49 2010 -0400
+++ b/Nominal/nominal_dt_supp.ML	Mon Sep 27 09:51:15 2010 -0400
@@ -186,6 +186,8 @@
         end)
   in
     induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
+    |> map atomize
+    |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]}))
   end