--- a/src/HOLCF/Porder0.ML Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOLCF/Porder0.ML Fri Sep 15 12:39:57 2000 +0200
@@ -12,7 +12,7 @@
(* minimal fixes least element *)
(* ------------------------------------------------------------------------ *)
Goal "!x::'a::po. uu<<x ==> uu=(@u.!y. u<<y)";
-by (blast_tac (claset() addIs [selectI2,antisym_less]) 1);
+by (blast_tac (claset() addIs [someI2,antisym_less]) 1);
bind_thm ("minimal2UU", allI RS result());
(* ------------------------------------------------------------------------ *)