src/ZF/List.ML

--- a/src/ZF/List.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/List.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -28,8 +28,7 @@
 
 goal List.thy "list(A) = {0} + (A * list(A))";
 let open list;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "list_unfold";