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 of persistent data;
authorwenzelm
Sat, 17 Feb 2018 17:34:31 +0100
changeset 67645 5e0c81750441
parent 67644 15c6256709d6
child 67646 85582dded912
trim context of persistent data;
src/ZF/Tools/typechk.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/Tools/typechk.ML	Sat Feb 17 17:34:15 2018 +0100
+++ b/src/ZF/Tools/typechk.ML	Sat Feb 17 17:34:31 2018 +0100
@@ -50,7 +50,7 @@
 
 val TC_add =
   Thm.declaration_attribute (fn thm => fn context =>
-    Data.map (add_rule (Context.proof_of context) thm) context);
+    Data.map (add_rule (Context.proof_of context) (Thm.trim_context thm)) context);
 
 val TC_del =
   Thm.declaration_attribute (fn thm => fn context =>
isabelle