--- a/src/HOLCF/Porder0.ML Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Porder0.ML Fri Oct 10 19:02:28 1997 +0200
@@ -12,7 +12,7 @@
(* ------------------------------------------------------------------------ *)
(* minimal fixes least element *)
(* ------------------------------------------------------------------------ *)
-bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po.uu<<x==>uu=(@u.!y.u<<y)"
+bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po. uu<<x==>uu=(@u.!y. u<<y)"
(fn prems =>
[
(cut_facts_tac prems 1),