# HG changeset patch
# User nipkow
# Date 878201246 -3600
# Node ID 5bb30bedbdc291673cadf1caff71a7f6653aeb2f
# Parent  43ec35b5054db09089cc4883fff2715a8aaee04d
Removed spurious blank.
Updated proof because of HOL change.

diff -r 43ec35b5054d -r 5bb30bedbdc2 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);
diff -r 43ec35b5054d -r 5bb30bedbdc2 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Oct 30 09:46:11 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Oct 30 09:47:26 1997 +0100
@@ -674,7 +674,7 @@
 by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);
 qed"ForallPFilterPid1";
 
-bind_thm(" ForallPFilterPid",ForallPFilterPid1 RS mp);
+bind_thm("ForallPFilterPid",ForallPFilterPid1 RS mp);
 
 
 (* holds also in other direction *)