# HG changeset patch
# User wenzelm
# Date 1440990734 -7200
# Node ID 0baa20dd768d8b357f2a639547e52979f0a4f540
# Parent  a2c6f7f64aca34b3429c1bf489734264ee843413
trim context for persistent storage;

diff -r a2c6f7f64aca -r 0baa20dd768d src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Aug 30 23:34:24 2015 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Aug 31 05:12:14 2015 +0200
@@ -575,15 +575,17 @@
 
 fun add_thmss _ _ [] ctxt = ctxt
   | add_thmss loc kind facts ctxt =
-      ctxt
-      |> Attrib.local_notes kind facts |> snd
-      |> Proof_Context.background_theory
-        ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
-          (* Registrations *)
-          (fn thy =>
-            fold_rev (fn (_, morph) =>
-              snd o Attrib.global_notes kind (Attrib.transform_facts morph facts))
-            (registrations_of (Context.Theory thy) loc) thy));
+      let val facts0 = (map o apsnd o map o apfst o map) Thm.trim_context facts in
+        ctxt
+        |> Attrib.local_notes kind facts |> snd
+        |> Proof_Context.background_theory
+          ((change_locale loc o apfst o apsnd) (cons ((kind, facts0), serial ())) #>
+            (* Registrations *)
+            (fn thy =>
+              fold_rev (fn (_, morph) =>
+                snd o Attrib.global_notes kind (Attrib.transform_facts morph facts))
+              (registrations_of (Context.Theory thy) loc) thy))
+      end;
 
 
 (* Declarations *)