src/HOLCF/Tools/Domain/domain_isomorphism.ML

 fun isodefl_const T =
   Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
 
 fun mk_deflation t =
   Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
-
-fun mk_lub t =
-  let
-    val T = Term.range_type (Term.fastype_of t);
-    val lub_const = Const (@{const_name lub}, (T --> boolT) --> T);
-    val UNIV_const = @{term "UNIV :: nat set"};
-    val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT;
-    val image_const = Const (@{const_name image}, image_type);
-  in
-    lub_const $ (image_const $ t $ UNIV_const)
-  end;
 
 (* splits a cterm into the right and lefthand sides of equality *)
 fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
 
 fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));