# HG changeset patch
# User huffman
# Date 1117834747 -7200
# Node ID fd980649c4b2c3b988c8097b0d852384f32e1cf0
# Parent  af5ed1a10cd7f333f9bf29d3f6cca380c4c1acc9
changed variable name in monofun_cfun_arg

diff -r af5ed1a10cd7 -r fd980649c4b2 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Fri Jun 03 23:38:12 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Fri Jun 03 23:39:07 2005 +0200
@@ -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"),("x","x>>xs")]  monofun_cfun_arg 1);
+by (dres_inst_tac [("f","HD"),("x","x>>xs")]  monofun_cfun_arg 1);
 by (Asm_full_simp_tac 1); 
 qed"divide_Seq";