diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/LCF/LCF.ML
--- a/src/LCF/LCF.ML	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/LCF/LCF.ML	Wed Jun 29 12:03:41 1994 +0200
@@ -65,7 +65,7 @@
 		      REPEAT(rstac(conjI::prems)1)]);
 
 val ext = prove_goal thy
-	"(!!x::'a::cpo. f(x)=g(x)::'b::cpo) ==> (%x.f(x))=(%x.g(x))"
+	"(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x.f(x))=(%x.g(x))"
 	(fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
 				    prem RS eq_imp_less1,
 				    prem RS eq_imp_less2]1)]);