diff -r 6a909ee1c2f0 -r 3bccde9cbb9d src/Pure/Isar/locale.ML
--- 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