diff -r c56aa8b59dc0 -r b94cd208f073 src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Lift3.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -139,13 +139,13 @@
 
 (* Two specific lemmas for the combination of LCF and HOL terms *)
 
-Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
+Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
 by (rtac cont2cont_CF1L 1);
 by (REPEAT (resolve_tac cont_lemmas1 1));
 by Auto_tac;
 qed"cont_fapp_app";
 
-Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
+Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
 by (rtac cont2cont_CF1L 1);
 by (etac cont_fapp_app 1);
 by (assume_tac 1);