diff -r 8abfb4f7bd02 -r f3fbbaeb4fb8 src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Wed Jul 25 13:13:01 2001 +0200
+++ b/src/HOLCF/Porder.ML	Wed Jul 25 13:33:08 2001 +0200
@@ -50,7 +50,7 @@
 bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
 
 Goal "EX x. M <<| x ==> M <<| lub(M)";
-by (asm_full_simp_tac (simpset() addsimps [lub, Ex_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [lub, some_eq_ex]) 1);
 bind_thm ("lubI", exI RS result());
 
 Goal "M <<| l ==> lub(M) = l";