src/HOL/Lambda/Eta.thy

--- a/src/HOL/Lambda/Eta.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Lambda/Eta.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -50,8 +50,7 @@
 lemma free_lift [simp]:
     "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
   apply (induct t fixing: i k)
-    apply (auto cong: conj_cong)
-  apply arith
+  apply (auto cong: conj_cong)
   done
 
 lemma free_subst [simp]: