| changeset 79369 | ecfba958ef16 |
| parent 79347 | 8aca79b3a9cb |
| child 79742 | 2e4518e8a36b |
--- a/src/Pure/Isar/attrib.ML Wed Dec 27 13:17:55 2023 +0100 +++ b/src/Pure/Isar/attrib.ML Wed Dec 27 15:00:48 2023 +0100 @@ -206,7 +206,7 @@ (* fact expressions *) fun global_notes kind facts thy = thy |> - Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts); + Global_Theory.note_thmss_foundation kind (map_facts (map (attribute_global thy)) facts); fun local_notes kind facts ctxt = ctxt |> Proof_Context.note_thmss kind (map_facts (map (attribute ctxt)) facts);