diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -45,7 +45,7 @@
 open Function_Common
 
 val simp_attribs =
-  @{attributes [simp, nitpick_simp]} @ [Code.add_default_eqn_attrib Code.Equation]
+  @{attributes [simp, nitpick_simp]}
 
 val psimp_attribs =
   @{attributes [nitpick_psimp]}
@@ -195,6 +195,7 @@
       in
         lthy
         |> add_simps I "simps" I simp_attribs tsimps
+        ||> Code.declare_default_eqns (map (rpair true) tsimps)
         ||>> Local_Theory.note
           ((derived_name defname "induct", [Attrib.case_names case_names]), tinduct)
         ||>> fold_map (note_derived ("elims", [Attrib.consumes 1, Attrib.constraints 1]))