src/ZF/ex/bt.ML

--- a/src/ZF/ex/bt.ML	Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/bt.ML	Fri Oct 15 10:25:23 1993 +0100
@@ -44,6 +44,5 @@
 			    Pair_in_univ]) 1);
 val bt_univ = result();
 
-val bt_subset_univ = standard (bt_mono RS (bt_univ RSN (2,subset_trans)));
+val bt_subset_univ = standard ([bt_mono, bt_univ] MRS subset_trans);
 
-