# HG changeset patch
# User huffman
# Date 1110239158 -3600
# Node ID 36f3e7ef3cb69d6d7d8f8846ec09dfb5b8eeab1d
# Parent  24d770bbc44adde4b8e10ebfa0956a38918ced7c
fixed variable name

diff -r 24d770bbc44a -r 36f3e7ef3cb6 src/HOLCF/IOA/meta_theory/Sequence.ML
--- 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";