Replaced split_tac by split_inside_tac.

--- a/src/HOL/Lambda/Lambda.ML	Mon May 06 15:21:05 1996 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Mon May 06 15:22:33 1996 +0200
@@ -77,7 +77,7 @@
 
 (*** subst and lift ***)
 
-fun addsplit ss = ss addsimps [subst_Var] setloop (split_tac [expand_if]);
+fun addsplit ss = ss addsimps [subst_Var] setloop (split_inside_tac [expand_if]);
 
 goal Lambda.thy "(Var k)[u/k] = u";
 by (asm_full_simp_tac(addsplit(!simpset)) 1);

--- a/src/HOL/MiniML/I.ML	Mon May 06 15:21:05 1996 +0200
+++ b/src/HOL/MiniML/I.ML	Mon May 06 15:22:33 1996 +0200
@@ -11,11 +11,11 @@
 
   (* case Var n *)
   by (simp_tac (!simpset addsimps [app_subst_list]
-      setloop (split_tac [expand_if])) 1);
+      setloop (split_inside_tac [expand_if])) 1);
   by (fast_tac (HOL_cs addss !simpset) 1);
 
  (* case Abs e *)
- by (asm_full_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+ by (asm_full_simp_tac (!simpset setloop (split_inside_tac [expand_bind])) 1);
  by (strip_tac 1);
  by (rtac conjI 1);
   by (strip_tac 1);
@@ -33,7 +33,7 @@
                              less_imp_le,lessI]) 1);
 
 (* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset setloop (split_inside_tac [expand_bind])) 1);
 by (strip_tac 1);
 by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1);
 by (rtac conjI 1);

--- a/src/ZF/Resid/Substitution.ML	Mon May 06 15:21:05 1996 +0200
+++ b/src/ZF/Resid/Substitution.ML	Mon May 06 15:22:33 1996 +0200
@@ -110,7 +110,7 @@
 by (asm_full_simp_tac (lift_ss) 1);
 val subst_App = result();
 
-fun addsplit ss = (ss setloop (split_tac [expand_if]) 
+fun addsplit ss = (ss setloop (split_inside_tac [expand_if]) 
                 addsimps [lift_rec_Var,subst_Var]);