# HG changeset patch
# User wenzelm
# Date 1192969305 -7200
# Node ID d91391a8705b9b543ffe70421edf42a4782a2a05
# Parent  de54445dc82c4a0658f9d966d041426b947ecdb5
avoid very slow metis invocation;

diff -r de54445dc82c -r d91391a8705b src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Oct 21 14:21:44 2007 +0200
+++ b/src/HOL/List.thy	Sun Oct 21 14:21:45 2007 +0200
@@ -2152,7 +2152,11 @@
  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)
+(*TOO SLOW
 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
+*)
+apply (erule_tac x = "Suc i" in allE, simp)
+apply (erule_tac x = "Suc j" in allE, simp)
 done
 
 lemma nth_eq_iff_index_eq: