diff -r 793bf5fa5fbf -r cea7cd0c7e99 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Fri Dec 16 13:37:08 2011 +0100
+++ b/src/HOL/Tools/Function/size.ML	Fri Dec 16 21:23:21 2011 +0100
@@ -202,12 +202,12 @@
     val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
       prove_size_eqs Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
 
-    val ([size_thms], thy'') =
-      Global_Theory.add_thmss
-        [((Binding.name "size", size_eqns),
-          [Simplifier.simp_add, Nitpick_Simps.add,
-           Thm.declaration_attribute
-               (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy';
+    val ([(_, size_thms)], thy'') = thy'
+      |> Global_Theory.note_thmss ""
+        [((Binding.name "size",
+            [Simplifier.simp_add, Nitpick_Simps.add,
+             Thm.declaration_attribute (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
+          [(size_eqns, [])])];
 
   in
     SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))