backlink definition to target `notes`
authorhaftmann
Mon, 09 Aug 2010 15:43:37 +0200
changeset 38300 502251f34bdc
parent 38299 b1738c40c2a7
child 38301 4647c2c81d74
backlink definition to target `notes`
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;