src/HOLCF/Tools/Domain/domain_axioms.ML
changeset 33802 48ce3a1063f2
parent 33801 e8535acd302c
child 33807 ce8d2e8bca21
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 16:50:25 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 17:53:22 2009 -0800
@@ -150,8 +150,8 @@
                    mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
 
   in (dnam,
-      if definitional then [reach_ax] else [abs_iso_ax, rep_iso_ax, reach_ax],
-      [when_def, copy_def] @
+      (if definitional then [reach_ax] else [abs_iso_ax, rep_iso_ax, reach_ax]),
+      (if definitional then [when_def] else [when_def, copy_def]) @
       con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
       [take_def, finite_def])
   end; (* let (calc_axioms) *)