src/HOLCF/IOA/meta_theory/RefCorrectness.ML

--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Thu Oct 30 09:46:11 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Thu Oct 30 09:47:26 1997 +0100
@@ -167,8 +167,6 @@
 
 by (rtac impI 1);
 by (Seq_Finite_induct_tac 1);
-(* base_case *)
-by (fast_tac HOL_cs 1);
 (* main case *)
 by (safe_tac set_cs);
 by (pair_tac "a" 1);