--- a/src/Pure/Isar/locale.ML Wed Sep 02 11:36:40 2015 +0200
+++ b/src/Pure/Isar/locale.ML Wed Sep 02 13:26:29 2015 +0200
@@ -575,8 +575,11 @@
local
-fun trim_context_facts facts =
- (map o apsnd o map o apfst o map) Thm.trim_context facts;
+val trim_fact = map Thm.trim_context;
+val trim_srcs = (map o Token.map_facts_src) trim_fact;
+
+fun trim_context_facts facts = facts |> map (fn ((b, atts), args) =>
+ ((b, trim_srcs atts), map (fn (a, more_atts) => (trim_fact a, trim_srcs more_atts)) args));
in