# 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;