Trancl.ML

--- a/Trancl.ML	Thu Aug 25 10:47:33 1994 +0200
+++ b/Trancl.ML	Thu Aug 25 11:01:45 1994 +0200
@@ -114,8 +114,7 @@
 \     !!x. P(<x,x>); \
 \     !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |] \
 \  ==>  P(<a,b>)";
-by (rtac (major RS (rtrancl_def RS def_induct)) 1);
-by (rtac rtrancl_fun_mono 1);
+by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
 by (fast_tac (comp_cs addIs prems) 1);
 val rtrancl_full_induct = result();