| changeset 1673 | d22110ddd0af |
| parent 1465 | 5d7a7e439cec |
| child 1894 | c2c8279d40f0 |
--- a/src/HOL/Lex/AutoChopper.ML Tue Apr 23 16:58:21 1996 +0200 +++ b/src/HOL/Lex/AutoChopper.ML Tue Apr 23 16:58:57 1996 +0200 @@ -150,7 +150,8 @@ by (fast_tac HOL_cs 2); by (Simp_tac 2); by (subgoal_tac "flat(yss) @ zs = list" 1); - by (Asm_simp_tac 1); + by(hyp_subst_tac 1); + by(atac 1); by (case_tac "yss = []" 1); by (Asm_simp_tac 1); by (hyp_subst_tac 1);