--- a/src/Pure/Isar/token.ML Sun Feb 18 17:57:14 2018 +0100
+++ b/src/Pure/Isar/token.ML Sun Feb 18 19:18:49 2018 +0100
@@ -70,6 +70,7 @@
val get_name: T -> name_value option
val declare_maxidx: T -> Proof.context -> Proof.context
val map_facts: (string option -> thm list -> thm list) -> T -> T
+ val trim_context_src: src -> src
val transform: morphism -> T -> T
val init_assignable: T -> T
val assign: value option -> T -> T
@@ -425,6 +426,8 @@
| Fact (a, ths) => Fact (a, f a ths)
| _ => v));
+val trim_context_src = (map o map_facts) (K (map Thm.trim_context));
+
(* transform *)