src/HOL/Induct/LList.ML
changeset 4818 90dab9f7d81e
parent 4521 c7f56322a84b
child 4831 dae4d63a1318
     1.1 --- a/src/HOL/Induct/LList.ML	Tue Apr 21 17:22:47 1998 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Tue Apr 21 17:23:24 1998 +0200
     1.3 @@ -651,7 +651,8 @@
     1.4  \    diag(llist(range Leaf))";
     1.5  by (rtac equalityI 1);
     1.6  by (fast_tac (claset() addIs [Rep_llist]) 1);
     1.7 -by (fast_tac (claset() addSEs [Abs_llist_inverse RS subst]) 1);
     1.8 +by (fast_tac (claset() delSWrapper "split_all_tac"
     1.9 +		       addSEs [Abs_llist_inverse RS subst]) 1);
    1.10  qed "prod_fun_range_eq_diag";
    1.11  
    1.12  (*Surprisingly hard to prove.  Used with lfilter*)