src/HOLCF/Tools/Domain/domain_axioms.ML
changeset 33809 033831fd9ef3
parent 33807 ce8d2e8bca21
child 33971 9c7fa7f76950
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 21:44:37 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 22:25:11 2009 -0800
@@ -150,7 +150,7 @@
                    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]),
+      (if definitional then [] 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])