src/HOLCF/Fun2.ML

--- a/src/HOLCF/Fun2.ML	Thu May 31 16:52:20 2001 +0200
+++ b/src/HOLCF/Fun2.ML	Thu May 31 16:52:32 2001 +0200
@@ -40,7 +40,7 @@
 (* chains of functions yield chains in the po range                         *)
 (* ------------------------------------------------------------------------ *)
 
-Goalw [chain] "chain(S::nat=>('a=>'b::po)) ==> chain(% i. S(i)(x))";
+Goalw [chain_def] "chain (S::nat=>('a=>'b::po)) ==> chain (%i. S i x)";
 by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1);
 qed "ch2ch_fun";