--- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 00:34:26 2010 -0800
@@ -164,7 +164,7 @@
) : cons;
val eqs : eq list =
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
- val thy = thy' |> Domain_Axioms.add_axioms false comp_dnam eqs;
+ val thy = thy' |> Domain_Axioms.add_axioms false eqs' comp_dnam eqs;
val ((rewss, take_rews), theorems_thy) =
thy
|> fold_map (fn (eq, (x,cs)) =>
@@ -237,7 +237,7 @@
) : cons;
val eqs : eq list =
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
- val thy = thy' |> Domain_Axioms.add_axioms true comp_dnam eqs;
+ val thy = thy' |> Domain_Axioms.add_axioms true eqs' comp_dnam eqs;
val ((rewss, take_rews), theorems_thy) =
thy
|> fold_map (fn (eq, (x,cs)) =>