diff -r 3d8acfae6fb8 -r 8cb42aa19358 src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Sat Feb 27 14:04:46 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Sat Feb 27 15:32:42 2010 -0800
@@ -78,15 +78,6 @@
           (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
       end;
 
-(* -- definitions concerning the discriminators - *)
-
-    val dis_defs = let
-      fun ddef (con,_,_) = (dis_name con ^"_def",%%:(dis_name con) == 
-                                              list_ccomb(%%:(dname^"_when"),map 
-                                                                              (fn (con',_,args) => (List.foldr /\#
-      (if con'=con then TT else FF) args)) cons))
-    in map ddef cons end;
-
     val mat_defs =
       let
         fun mdef (con, _, _) =
@@ -134,7 +125,7 @@
   in (dnam,
       (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
       (if definitional then [when_def] else [when_def, copy_def]) @
-      dis_defs @ mat_defs @ pat_defs @
+      mat_defs @ pat_defs @
       [take_def, finite_def])
   end; (* let (calc_axioms) *)