# HG changeset patch
# User wenzelm
# Date 1320787379 -3600
# Node ID 117ff038f8f7f4ded32ba72d275c4c1eb9b43a24
# Parent  7797f5351ec4723896e8fc9da3080d98865306e7
disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;

diff -r 7797f5351ec4 -r 117ff038f8f7 src/Pure/Isar/generic_target.ML
--- 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) =