# HG changeset patch
# User wenzelm
# Date 1332411111 -3600
# Node ID bfad2f674d0ea3b379a8292f7902f9a277cf4871
# Parent  6231adc3895d8af404af8d840d1285cb09d31fb2
tuned;

diff -r 6231adc3895d -r bfad2f674d0e src/Pure/Isar/generic_target.ML
--- 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;
 
 
diff -r 6231adc3895d -r bfad2f674d0e src/Pure/Isar/named_target.ML
--- 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
diff -r 6231adc3895d -r bfad2f674d0e src/Pure/Isar/specification.ML
--- 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;