don't bother returning con_defs
authorhuffman
Fri Feb 26 09:13:29 2010 -0800 (2010-02-26)
changeset 35451a726a033b313
parent 35450 e9ef2b50ac59
child 35452 cf8c5a751a9a
don't bother returning con_defs
src/HOLCF/Tools/Domain/domain_constructors.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri Feb 26 09:10:50 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri Feb 26 09:13:29 2010 -0800
     1.3 @@ -14,7 +14,7 @@
     1.4        -> thm * thm
     1.5        -> theory
     1.6        -> { con_consts : term list,
     1.7 -           con_defs : thm list,
     1.8 +           con_betas : thm list,
     1.9             con_compacts : thm list,
    1.10             sel_rews : thm list }
    1.11           * theory;
    1.12 @@ -514,7 +514,6 @@
    1.13      val result =
    1.14        {
    1.15          con_consts = con_consts,
    1.16 -        con_defs = con_defs,
    1.17          con_betas = con_betas,
    1.18          con_compacts = con_compacts
    1.19        };
    1.20 @@ -543,7 +542,7 @@
    1.21      val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
    1.22  
    1.23      (* define constructor functions *)
    1.24 -    val ({con_consts, con_defs, con_betas, con_compacts}, thy) =
    1.25 +    val ({con_consts, con_betas, con_compacts}, thy) =
    1.26          add_constructors spec abs_const iso_locale thy;
    1.27  
    1.28      (* TODO: enable this earlier *)
    1.29 @@ -563,7 +562,7 @@
    1.30  
    1.31      val result =
    1.32        { con_consts = con_consts,
    1.33 -        con_defs = con_defs,
    1.34 +        con_betas = con_betas,
    1.35          con_compacts = con_compacts,
    1.36          sel_rews = sel_thms };
    1.37    in
     2.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Feb 26 09:10:50 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Feb 26 09:13:29 2010 -0800
     2.3 @@ -197,7 +197,7 @@
     2.4      (Long_Name.base_name dname) dom_eqn
     2.5      (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) thy;
     2.6  
     2.7 -val axs_con_def = #con_defs result;
     2.8 +val con_appls = #con_betas result;
     2.9  val con_compacts = #con_compacts result;
    2.10  val sel_rews = #sel_rews result;
    2.11  
    2.12 @@ -244,8 +244,6 @@
    2.13  
    2.14  val _ = trace "Proving when_appl...";
    2.15  val when_appl = appl_of_def ax_when_def;
    2.16 -val _ = trace "Proving con_appls...";
    2.17 -val con_appls = map appl_of_def axs_con_def;
    2.18  
    2.19  local
    2.20    fun arg2typ n arg =