src/ZF/List.ML

--- a/src/ZF/List.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/List.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -52,8 +52,7 @@
 			    Pair_in_univ]) 1);
 val list_univ = result();
 
-val list_subset_univ = standard
-    (list_mono RS (list_univ RSN (2,subset_trans)));
+val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans);
 
 val major::prems = goal List.thy
     "[| l: list(A);    \