src/HOL/List.thy

--- a/src/HOL/List.thy	Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/List.thy	Mon Sep 30 16:14:02 2002 +0200
@@ -1268,10 +1268,9 @@
  apply simp
  apply blast
 apply (simp add: image_Collect lex_prod_def)
-apply auto
+apply safe
 apply blast
- apply (rename_tac a xys x xs' y ys')
- apply (rule_tac x = "a # xys" in exI)
+ apply (rule_tac x = "ab # xys" in exI)
  apply simp
 apply (case_tac xys)
  apply simp_all