--- 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();