tuned;

--- a/src/Pure/Isar/generic_target.ML	Thu Mar 22 10:49:31 2012 +0100
+++ b/src/Pure/Isar/generic_target.ML	Thu Mar 22 11:11:51 2012 +0100
@@ -88,8 +88,7 @@
 
     (*note*)
     val ([(res_name, [res])], lthy4) = lthy3
-      |> Local_Theory.notes_kind ""
-        [((if internal then Binding.empty else b_def, atts), [([def], [])])];
+      |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
   in ((lhs, (res_name, res)), lthy4) end;
 
 

--- a/src/Pure/Isar/named_target.ML	Thu Mar 22 10:49:31 2012 +0100
+++ b/src/Pure/Isar/named_target.ML	Thu Mar 22 11:11:51 2012 +0100
@@ -133,7 +133,7 @@
     lthy
     |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
     |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
-  end
+  end;
 
 fun target_notes (Target {target, is_locale, ...}) =
   if is_locale then locale_notes target

--- a/src/Pure/Isar/specification.ML	Thu Mar 22 10:49:31 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 22 11:11:51 2012 +0100
@@ -220,8 +220,7 @@
     val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
 
     val ([(def_name, [th'])], lthy4) = lthy3
-      |> Local_Theory.notes_kind ""
-        [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
+      |> Local_Theory.notes [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
 
     val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;