changeset 35495 | dc59e781669f |
parent 35494 | 45c9a8278faf |
child 35497 | 979706bd5c16 |
--- 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