# HG changeset patch
# User huffman
# Date 1267204409 28800
# Node ID a726a033b3135b56c9e4343e35100c83e4d5bce3
# Parent  e9ef2b50ac59d494b4f723ad48f4ef90e9815a7c
don't bother returning con_defs

diff -r e9ef2b50ac59 -r a726a033b313 src/HOLCF/Tools/Domain/domain_constructors.ML
--- 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
diff -r e9ef2b50ac59 -r a726a033b313 src/HOLCF/Tools/Domain/domain_theorems.ML
--- 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 =