diff -r 88f15198950f -r bdeb5024353a src/ZF/List.ML
--- a/src/ZF/List.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/List.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -28,7 +28,7 @@
 
 goal List.thy "list(A) = {0} + (A * list(A))";
 let open list;  val rew = rewrite_rule con_defs in  
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
                      addEs [rew elim]) 1)
 end;
 qed "list_unfold";
@@ -113,7 +113,7 @@
 
 goalw List.thy [drop_def]
     "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
-br sym 1;
+by (rtac sym 1);
 by (etac nat_induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);