--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Tue Mar 08 00:32:10 2005 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Tue Mar 08 00:45:58 2005 +0100
@@ -1,6 +1,6 @@
(* Title: HOLCF/IOA/meta_theory/Sequence.ML
ID: $Id$
- Author: Olaf Müller
+ Author: Olaf Mller
Theorems about Sequences over flat domains with lifted elements.
*)
@@ -806,7 +806,7 @@
\ ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) \
\ & Finite (Takewhile (%a. ~ P a)$y) & P x";
by (rtac (divide_Seq_lemma RS mp) 1);
-by (dres_inst_tac [("fo","HD"),("xa","x>>xs")] monofun_cfun_arg 1);
+by (dres_inst_tac [("fo","HD"),("x","x>>xs")] monofun_cfun_arg 1);
by (Asm_full_simp_tac 1);
qed"divide_Seq";