--- 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 =