src/HOL/Tools/Old_Datatype/old_size.ML

--- a/src/HOL/Tools/Old_Datatype/old_size.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_size.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -196,8 +196,7 @@
           |> Global_Theory.note_thmss ""
             [((Binding.name "size",
                 [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp},
-                 Thm.declaration_attribute (fn thm =>
-                   Context.mapping (Code.add_default_eqn thm) I)]),
+                 Code.add_default_eqn_attribute Code.Equation]),
               [(size_eqns, [])])];
 
       in