src/HOLCF/Discrete.ML

--- a/src/HOLCF/Discrete.ML	Thu May 31 16:52:20 2001 +0200
+++ b/src/HOLCF/Discrete.ML	Thu May 31 16:52:32 2001 +0200
@@ -14,7 +14,7 @@
 by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
 qed "discr_chain_f_range0";
 
-Goalw [cont,is_lub,is_ub] "cont(%x::('a::term)discr. f x)";
+Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::term)discr. f x)";
 by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
 qed "cont_discr";
 AddIffs [cont_discr];