| changeset 1723 | 286f9b6370ab |
| parent 1673 | d22110ddd0af |
| child 1759 | a42d6c537f4a |
--- 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);