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.
disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;
authorwenzelm
Tue, 08 Nov 2011 22:22:59 +0100
changeset 45413 117ff038f8f7
parent 45412 7797f5351ec4
child 45414 8ca612982014
disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;
src/Pure/Isar/generic_target.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/generic_target.ML	Tue Nov 08 21:09:35 2011 +0100
+++ b/src/Pure/Isar/generic_target.ML	Tue Nov 08 22:22:59 2011 +0100
@@ -117,7 +117,7 @@
       |> Drule.zero_var_indexes_list;
 
     (*thm definition*)
-    val result = Global_Theory.name_thm true true name (Thm.compress th'');
+    val result = Global_Theory.name_thm true true name th'';
 
     (*import fixes*)
     val (tvars, vars) =
isabelle