# HG changeset patch # User wenzelm # Date 1465568928 -7200 # Node ID 6c963f1fc3886ebff65af101f93c14611d9e0a1a # Parent e6d51d9801e451989ad680d11436f65ad4cd5bdf avoid duplicate Attrib.local_notes in aux. context; diff -r e6d51d9801e4 -r 6c963f1fc388 src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Fri Jun 10 16:17:33 2016 +0200 +++ b/src/Pure/Isar/bundle.ML Fri Jun 10 16:28:48 2016 +0200 @@ -159,7 +159,7 @@ in lthy |> augment_target (transform_bundle (Local_Theory.standard_morphism_theory lthy) bundle) - |> Generic_Target.standard_notes (K true) kind facts + |> Generic_Target.standard_notes (op <>) kind facts |> Attrib.local_notes kind facts end;