diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/Resid/Substitution.ML
--- a/src/ZF/Resid/Substitution.ML	Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/Resid/Substitution.ML	Thu Jul 02 17:58:12 1998 +0200
@@ -108,7 +108,7 @@
 by (asm_full_simp_tac (simpset()) 1);
 qed "subst_App";
 
-fun addsplit ss = (ss setloop (split_inside_tac [expand_if]) 
+fun addsplit ss = (ss setloop (split_inside_tac [split_if]) 
                 addsimps [lift_rec_Var,subst_Var]);