# HG changeset patch
# User haftmann
# Date 1281361417 -7200
# Node ID 502251f34bdc49e097ea1a1ad12211f37470e0ac
# Parent  b1738c40c2a77807e091dfe5b76f920bdf2fd8d9
backlink definition to target `notes`

diff -r b1738c40c2a7 -r 502251f34bdc src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Aug 09 15:40:25 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Aug 09 15:43:37 2010 +0200
@@ -358,7 +358,7 @@
 
     (*note*)
     val ([(res_name, [res])], lthy5) = lthy4
-      |> notes ta "" [((name', atts), [([def], [])])];
+      |> Local_Theory.notes_kind "" [((name', atts), [([def], [])])];
   in ((lhs, (res_name, res)), lthy5) end;
 
 end;