# HG changeset patch
# User wenzelm
# Date 1441193189 -7200
# Node ID 3bccde9cbb9db63bf892e0e9d793c97dc6905746
# Parent  6a909ee1c2f0ec67406b78cbffa5f6d180433cdd
trim context more thoroughly;

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
 
diff -r 6a909ee1c2f0 -r 3bccde9cbb9d src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Sep 02 11:36:40 2015 +0200
+++ b/src/Pure/Isar/token.ML	Wed Sep 02 13:26:29 2015 +0200
@@ -77,6 +77,8 @@
   val map_values: (value -> value) -> src -> src
   val declare_maxidx: T -> Proof.context -> Proof.context
   val declare_maxidx_src: src -> Proof.context -> Proof.context
+  val map_facts: (thm list -> thm list) -> T -> T
+  val map_facts_src: (thm list -> thm list) -> src -> src
   val transform: morphism -> T -> T
   val transform_src: morphism -> src -> src
   val init_assignable: T -> T
@@ -437,6 +439,17 @@
 and declare_maxidx_src src = fold declare_maxidx (args_of_src src);
 
 
+(* fact values *)
+
+fun map_facts f =
+  map_value (fn v =>
+    (case v of
+      Source src => Source (map_facts_src f src)
+    | Fact (a, ths) => Fact (a, f ths)
+    | _ => v))
+and map_facts_src f = map_args (map_facts f);
+
+
 (* transform *)
 
 fun transform phi =