src/ZF/Resid/Substitution.ML

     "!!n.[|p:nat; u:redexes|]==>  \
 \        subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
 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]);
 
 
 goal Substitution.thy  
     "!!n.u:redexes ==> ALL k:nat.lift_rec(u,k):redexes";