src/HOLCF/Tools/Domain/domain_theorems.ML

 val (result, thy) =
   Domain_Constructors.add_domain_constructors
     (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;
 
 (* ----- theorems concerning the isomorphism -------------------------------- *)
 

     in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
 end;
 
 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 =
     let val t = TVar (("'a", n), pcpoS)
     in (n + 1, if is_lazy arg then mk_uT t else t) end;