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:53:14 +0200
changeset 61091 2b7ef52a4ea9
parent 61090 16f7f9aa4263
child 61092 d261ac466180
trim context for persistent storage;
src/Pure/Isar/local_defs.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/local_defs.ML	Wed Sep 02 20:14:19 2015 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Sep 02 21:53:14 2015 +0200
@@ -178,8 +178,8 @@
   Pretty.writeln (Pretty.big_list "definitional rewrite rules:"
     (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
 
-val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
-val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
+val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm o Thm.trim_context);
+val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm o Thm.trim_context);
 
 
 (* meta rewrite rules *)
isabelle