# HG changeset patch
# User paulson
# Date 1190203153 -7200
# Node ID 1e8053a6d725b4d6ea65151740820e24193fe291
# Parent  212c9b342a67970bd5b5e3da66114a2c5f613f3c
metis too slow

diff -r 212c9b342a67 -r 1e8053a6d725 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Sep 19 13:52:54 2007 +0200
+++ b/src/HOL/List.thy	Wed Sep 19 13:59:13 2007 +0200
@@ -2112,9 +2112,14 @@
 apply (case_tac j, simp)
 apply (simp add: set_conv_nth)
  apply (case_tac j)
-apply (clarsimp simp add: set_conv_nth, simp)
+apply (clarsimp simp add: set_conv_nth, simp) 
 apply (rule conjI)
+(*TOO SLOW
 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
+*)
+ apply (clarsimp simp add: set_conv_nth)
+ apply (erule_tac x = 0 in allE, simp)
+ apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
 done