Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
trim context for persistent storage;
authorwenzelm
Wed, 02 Sep 2015 21:54:00 +0200
changeset 61092 d261ac466180
parent 61091 2b7ef52a4ea9
child 61093 0f48b7b80e88
trim context for persistent storage;
src/Pure/Isar/object_logic.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle