diff -r 0b9b8eb74101 -r b7f57e0ab47c ex/Term.ML
--- a/ex/Term.ML	Thu Aug 18 12:42:19 1994 +0200
+++ b/ex/Term.ML	Thu Aug 18 12:48:03 1994 +0200
@@ -145,9 +145,9 @@
     "[| M: Sexp;  N: List(Term(A));  A<=Sexp |] ==> \
 \    Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
 by (rtac (Term_rec_unfold RS trans) 1);
-by (rtac (Split RS trans) 1);
 by (simp_tac (HOL_ss addsimps
-      [prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl,
+      [Split,
+       prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl,
        prem1, prem2 RS rev_subsetD, List_subset_Sexp,
        Term_subset_Sexp, A_subset_Sexp])1);
 val Term_rec = result();