# HG changeset patch
# User wenzelm
# Date 1441223640 -7200
# Node ID d261ac4661802d4073cc98e6fa0f6e727513d01f
# Parent  2b7ef52a4ea9aca013425a6435299e0a80de8f4b
trim context for persistent storage;

diff -r 2b7ef52a4ea9 -r d261ac466180 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Sep 02 21:53:14 2015 +0200
+++ b/src/Pure/Isar/object_logic.ML	Wed Sep 02 21:54:00 2015 +0200
@@ -166,10 +166,10 @@
 val get_rulify = #2 o #atomize_rulify o get_data;
 
 fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
-  (base_sort, judgment, (Thm.add_thm th atomize, rulify)));
+  (base_sort, judgment, (Thm.add_thm (Thm.trim_context th) atomize, rulify)));
 
 fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
-  (base_sort, judgment, (atomize, Thm.add_thm th rulify)));
+  (base_sort, judgment, (atomize, Thm.add_thm (Thm.trim_context th) rulify)));
 
 val declare_atomize = Thm.declaration_attribute add_atomize;
 val declare_rulify = Thm.declaration_attribute add_rulify;