move function mk_lub into holcf_library.ML

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 02 20:43:41 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Mar 03 06:25:42 2010 -0800
@@ -106,17 +106,6 @@
 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);
 

--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Mar 02 20:43:41 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Mar 03 06:25:42 2010 -0800
@@ -116,17 +116,6 @@
 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);
 

--- a/src/HOLCF/Tools/holcf_library.ML	Tue Mar 02 20:43:41 2010 -0800
+++ b/src/HOLCF/Tools/holcf_library.ML	Wed Mar 03 06:25:42 2010 -0800
@@ -9,6 +9,7 @@
 
 infixr 6 ->>;
 infix -->>;
+infix 9 `;
 
 (*** Operations from Isabelle/HOL ***)
 
@@ -47,6 +48,17 @@
 fun mk_chain t =
   Const (@{const_name chain}, 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;
+
 
 (*** Continuous function space ***)
 
@@ -88,7 +100,7 @@
       | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
   in capply_const (S, T) $ t $ u end;
 
-infix 9 ` ; val (op `) = mk_capply;
+val (op `) = mk_capply;
 
 val list_ccomb : term * term list -> term = Library.foldl mk_capply;