--- 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])