--- 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;