src/HOL/Library/old_recdef.ML
changeset 63239 d562c9948dee
parent 62058 1cfd5d604937
child 64556 851ae0e7b09c
--- a/src/HOL/Library/old_recdef.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Library/old_recdef.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -2834,7 +2834,7 @@
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     val simp_att =
       if null tcs then [Simplifier.simp_add,
-        Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute]
+        Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute Code.Equation]
       else [];
     val ((simps' :: rules', [induct']), thy2) =
       Proof_Context.theory_of ctxt1