diff -r ae9a2ea9a989 -r 02b7738aef6a src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -367,11 +367,10 @@
       (fn thss => fn goal_ctxt =>
          let
            val simps = ProofContext.export goal_ctxt lthy' (flat thss);
-           val (simps', lthy'') = fold_map (LocalTheory.note "")
-             (names_atts' ~~ map single simps) lthy'
+           val (simps', lthy'') = fold_map LocalTheory.note (names_atts' ~~ map single simps) lthy';
          in
            lthy''
-           |> LocalTheory.note "" ((qualify (Binding.name "simps"),
+           |> LocalTheory.note ((qualify (Binding.name "simps"),
                 map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
                 maps snd simps')
            |> snd