# HG changeset patch
# User paulson
# Date 996060788 -7200
# Node ID f3fbbaeb4fb8ae8782ed0efab7ecaad1e1dfdf6c
# Parent  8abfb4f7bd02185762ea89716e7e5b7309b0974c
removed reference to Ex_def

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";