src/HOLCF/Tools/Domain/domain_syntax.ML

     fun dbind s = Binding.name (dnam ^ s);
     val const_rep  = (dbind "_rep" ,              dtype  ->> dtype2, NoSyn);
     val const_abs  = (dbind "_abs" ,              dtype2 ->> dtype , NoSyn);
     end;
 
-    val const_finite = (dbind "_finite", dtype-->HOLogic.boolT       , NoSyn);
-
     val optional_consts =
         if definitional then [] else [const_rep, const_abs];
 
-  in (optional_consts @ [const_finite])
+  in optional_consts
   end; (* let *)
 
 (* ----- putting all the syntax stuff together ------------------------------ *)
 
 fun add_syntax