# HG changeset patch
# User oheimb
# Date 893172204 -7200
# Node ID 90dab9f7d81eab0d97d9e65de4b2cc757de21aad
# Parent  8b81289852e394a29d670ac5a27c72c2dff1aeda
split_all_tac is now added to claset() _before_ other safe tactics

diff -r 8b81289852e3 -r 90dab9f7d81e 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*)