src/HOLCF/IOA/meta_theory/Sequence.ML
changeset 4716 a291e858061c
parent 4681 a331c1f5a23e
child 4721 c8a8482a8124
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Mar 10 14:27:44 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Mar 10 16:47:26 1998 +0100
@@ -414,8 +414,6 @@
 (* nil*)
 by (strip_tac 1);
 by (Seq_case_simp_tac "x" 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 (* cons *)
 by (strip_tac 1);