diff -r ae9a2ea9a989 -r 02b7738aef6a src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -277,8 +277,8 @@
     lthy
     |> set_group ? LocalTheory.set_group (serial ())
     |> add_primrec_simple fixes (map snd spec)
-    |-> (fn (prefix, simps) => fold_map (LocalTheory.note "") (attr_bindings prefix ~~ simps)
-      #-> (fn simps' => LocalTheory.note "" (simp_attr_binding prefix, maps snd simps')))
+    |-> (fn (prefix, simps) => fold_map LocalTheory.note (attr_bindings prefix ~~ simps)
+      #-> (fn simps' => LocalTheory.note (simp_attr_binding prefix, maps snd simps')))
     |>> snd
   end;