src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35451 a726a033b313
parent 35448 f9f73f0475eb
child 35452 cf8c5a751a9a
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Feb 26 09:10:50 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Feb 26 09:13:29 2010 -0800
     1.3 @@ -197,7 +197,7 @@
     1.4      (Long_Name.base_name dname) dom_eqn
     1.5      (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) thy;
     1.6  
     1.7 -val axs_con_def = #con_defs result;
     1.8 +val con_appls = #con_betas result;
     1.9  val con_compacts = #con_compacts result;
    1.10  val sel_rews = #sel_rews result;
    1.11  
    1.12 @@ -244,8 +244,6 @@
    1.13  
    1.14  val _ = trace "Proving when_appl...";
    1.15  val when_appl = appl_of_def ax_when_def;
    1.16 -val _ = trace "Proving con_appls...";
    1.17 -val con_appls = map appl_of_def axs_con_def;
    1.18  
    1.19  local
    1.20    fun arg2typ n arg =