src/HOL/Induct/LList.ML

--- a/src/HOL/Induct/LList.ML	Tue Apr 21 17:22:47 1998 +0200
+++ b/src/HOL/Induct/LList.ML	Tue Apr 21 17:23:24 1998 +0200
@@ -651,7 +651,8 @@
 \    diag(llist(range Leaf))";
 by (rtac equalityI 1);
 by (fast_tac (claset() addIs [Rep_llist]) 1);
-by (fast_tac (claset() addSEs [Abs_llist_inverse RS subst]) 1);
+by (fast_tac (claset() delSWrapper "split_all_tac"
+		       addSEs [Abs_llist_inverse RS subst]) 1);
 qed "prod_fun_range_eq_diag";
 
 (*Surprisingly hard to prove.  Used with lfilter*)