--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Fri Feb 26 09:10:50 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Fri Feb 26 09:13:29 2010 -0800
@@ -14,7 +14,7 @@
-> thm * thm
-> theory
-> { con_consts : term list,
- con_defs : thm list,
+ con_betas : thm list,
con_compacts : thm list,
sel_rews : thm list }
* theory;
@@ -514,7 +514,6 @@
val result =
{
con_consts = con_consts,
- con_defs = con_defs,
con_betas = con_betas,
con_compacts = con_compacts
};
@@ -543,7 +542,7 @@
val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
(* define constructor functions *)
- val ({con_consts, con_defs, con_betas, con_compacts}, thy) =
+ val ({con_consts, con_betas, con_compacts}, thy) =
add_constructors spec abs_const iso_locale thy;
(* TODO: enable this earlier *)
@@ -563,7 +562,7 @@
val result =
{ con_consts = con_consts,
- con_defs = con_defs,
+ con_betas = con_betas,
con_compacts = con_compacts,
sel_rews = sel_thms };
in
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Feb 26 09:10:50 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Feb 26 09:13:29 2010 -0800
@@ -197,7 +197,7 @@
(Long_Name.base_name dname) dom_eqn
(rep_const, abs_const) (ax_rep_iso, ax_abs_iso) thy;
-val axs_con_def = #con_defs result;
+val con_appls = #con_betas result;
val con_compacts = #con_compacts result;
val sel_rews = #sel_rews result;
@@ -244,8 +244,6 @@
val _ = trace "Proving when_appl...";
val when_appl = appl_of_def ax_when_def;
-val _ = trace "Proving con_appls...";
-val con_appls = map appl_of_def axs_con_def;
local
fun arg2typ n arg =