# HG changeset patch # User wenzelm # Date 1682105189 -7200 # Node ID acee6c7fafff799aeefb69b5b44b51e8923c5556 # Parent e7fd273657f188536c1a1f6aa0405ba04ad6b5f3 proper Thm.trim_context / Thm.transfer (see also 0d401f874942); diff -r e7fd273657f1 -r acee6c7fafff src/Pure/Tools/named_thms.ML --- a/src/Pure/Tools/named_thms.ML Fri Apr 21 21:25:10 2023 +0200 +++ b/src/Pure/Tools/named_thms.ML Fri Apr 21 21:26:29 2023 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/Tools/named_thms.ML Author: Makarius -Named collections of theorems in canonical order. +Named collections of theorems in canonical (reverse) order: OLD VERSION. *) signature NAMED_THMS = @@ -27,10 +27,10 @@ val member = Item_Net.member o Data.get o Context.Proof; -val content = Item_Net.content o Data.get; +fun content context = map (Thm.transfer'' context) (Item_Net.content (Data.get context)); val get = content o Context.Proof; -val add_thm = Data.map o Item_Net.update; +val add_thm = Data.map o Item_Net.update o Thm.trim_context; val del_thm = Data.map o Item_Net.remove; val add = Thm.declaration_attribute add_thm;