diff -r 60b7800338d5 -r 18f426a137a9 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Jul 11 11:54:03 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Jul 11 11:54:21 2007 +0200
@@ -355,7 +355,7 @@
 
 lemma Seq_Finite_ind:
 "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x"
-apply (erule (1) sfinite.induct)
+apply (erule (1) Finite.induct)
 apply (tactic {* def_tac 1 *})
 apply (simp add: Consq_def)
 done