# HG changeset patch
# User wenzelm
# Date 1518813832 -3600
# Node ID e4eb21f8331c35a707e978003a73dfff52f8a8e5
# Parent  28f926146986da21ef951a25e78dac26664eee26
trim context of persistent data;

diff -r 28f926146986 -r e4eb21f8331c src/HOL/Nonstandard_Analysis/transfer_principle.ML
--- a/src/HOL/Nonstandard_Analysis/transfer_principle.ML	Fri Feb 16 21:40:15 2018 +0100
+++ b/src/HOL/Nonstandard_Analysis/transfer_principle.ML	Fri Feb 16 21:43:52 2018 +0100
@@ -108,13 +108,13 @@
     {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
 in
 
-val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm);
+val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm o Thm.trim_context);
 val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm);
 
-val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm);
+val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm o Thm.trim_context);
 val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm);
 
-val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm);
+val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm o Thm.trim_context);
 val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm);
 
 end