diff -r 45c9a8278faf -r dc59e781669f src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 00:34:26 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 02:28:45 2010 -0800
@@ -209,8 +209,6 @@
           if definitional then thy
           else fold ax_lub_take dnames thy
     end;
-
-    val use_copy_def = length eqs>1 andalso not definitional;
   in
     thy
     |> Sign.add_path comp_dnam