src/HOLCF/Tools/Domain/domain_axioms.ML
changeset 33807 ce8d2e8bca21
parent 33802 48ce3a1063f2
child 33809 033831fd9ef3
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 20:09:56 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 21:06:22 2009 -0800
@@ -241,10 +241,11 @@
     val thy = thy'
       |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs);
 
+    val use_copy_def = length eqs>1 andalso not definitional;
   in
     thy
     |> Sign.add_path comp_dnam  
-    |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
+    |> add_defs_infer (bisim_def::(if use_copy_def then [copy_def] else []))
     |> Sign.parent_path
     |> fold add_matchers eqs
   end; (* let (add_axioms) *)