src/HOLCF/Tools/Domain/domain_theorems.ML

 local
   fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
 in
   val ax_abs_iso  = ga "abs_iso"  dname;
   val ax_rep_iso  = ga "rep_iso"  dname;
-  val ax_when_def = ga "when_def" dname;
   val ax_copy_def = ga "copy_def" dname;
 end; (* local *)
 
 (* ----- define constructors ------------------------------------------------ *)
 

     rep_inverse = ax_rep_iso
   };
 
 val (result, thy) =
   Domain_Constructors.add_domain_constructors
-    (Long_Name.base_name dname) (snd dom_eqn) iso_info ax_when_def thy;
+    (Long_Name.base_name dname) (snd dom_eqn) iso_info thy;
 
 val con_appls = #con_betas result;
 val {exhaust, casedist, ...} = result;
 val {con_compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
 val {sel_rews, ...} = result;