--- 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]))