--- a/src/Pure/Isar/attrib.ML Fri Feb 16 14:11:25 2018 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Feb 16 18:25:35 2018 +0100
@@ -29,6 +29,7 @@
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
type thms = (thm list * Token.src list) list
+ val trim_context: thms -> thms
val global_notes: string -> (Attrib.binding * thms) list ->
theory -> (string * thm list) list * theory
val local_notes: string -> (Attrib.binding * thms) list ->
@@ -181,6 +182,8 @@
type thms = (thm list * Token.src list) list;
+val trim_context: thms -> thms = (map o apfst o map) Thm.trim_context;
+
fun global_notes kind facts thy = thy |>
Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);