# HG changeset patch
# User wenzelm
# Date 1518801935 -3600
# Node ID d4cb46bc836048a1b4226e11c7a6cb6e80da42a3
# Parent  dee9d2924617128eef1ddc8a6a97053c46bec1a4
more operations;

diff -r dee9d2924617 -r d4cb46bc8360 src/Pure/Isar/attrib.ML
--- 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);