# HG changeset patch
# User wenzelm
# Date 1291214140 -3600
# Node ID 15b97bd4b5c02a0c8c804b7a4f409162be797d10
# Parent  5895c525739da4af28afb5ceb28288c631e1ffcf
just one HOLogic.mk_comp;

diff -r 5895c525739d -r 15b97bd4b5c0 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Dec 01 15:03:44 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Dec 01 15:35:40 2010 +0100
@@ -87,14 +87,6 @@
     Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
   end;
 
-fun mk_fun_comp (t, u) =
-  let
-    val (_, B) = dest_funT (fastype_of t)
-    val (C, A) = dest_funT (fastype_of u)
-  in
-    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
-  end;
-
 fun dest_randomT (Type ("fun", [@{typ Random.seed},
   Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
   | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
diff -r 5895c525739d -r 15b97bd4b5c0 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Wed Dec 01 15:03:44 2010 +0100
+++ b/src/HOL/Tools/hologic.ML	Wed Dec 01 15:35:40 2010 +0100
@@ -8,6 +8,7 @@
 sig
   val typeS: sort
   val typeT: typ
+  val mk_comp: term * term -> term
   val boolN: string
   val boolT: typ
   val Trueprop: term
@@ -142,6 +143,16 @@
 val typeT = Type_Infer.anyT typeS;
 
 
+(* functions *)
+
+fun mk_comp (f, g) =
+  let
+    val fT = fastype_of f;
+    val gT = fastype_of g;
+    val compT = fT --> gT --> domain_type gT --> range_type fT;
+  in Const ("Fun.comp", compT) $ f $ g end;
+
+
 (* bool and set *)
 
 val boolN = "HOL.bool";
diff -r 5895c525739d -r 15b97bd4b5c0 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Dec 01 15:03:44 2010 +0100
+++ b/src/HOL/Tools/record.ML	Wed Dec 01 15:35:40 2010 +0100
@@ -1013,17 +1013,9 @@
     SOME u_name => u_name = s
   | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
 
-fun mk_comp f g =
-  let
-    val X = fastype_of g;
-    val (A, B) = dest_funT X;
-    val C = range_type (fastype_of f);
-    val T = (B --> C) --> (A --> B) --> A --> C;
-  in Const (@{const_name Fun.comp}, T) $ f $ g end;
-
 fun mk_comp_id f =
   let val T = range_type (fastype_of f)
-  in mk_comp (Const (@{const_name Fun.id}, T --> T)) f end;
+  in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;
 
 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
   | get_upd_funs _ = [];
@@ -1036,10 +1028,10 @@
       let
         (* FIXME fresh "f" (!?) *)
         val T = domain_type (fastype_of upd);
-        val lhs = mk_comp acc (upd $ Free ("f", T));
+        val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
         val rhs =
           if is_sel_upd_pair thy acc upd
-          then mk_comp (Free ("f", T)) acc
+          then HOLogic.mk_comp (Free ("f", T), acc)
           else mk_comp_id acc;
         val prop = lhs === rhs;
         val othm =
@@ -1060,11 +1052,11 @@
     (* FIXME fresh "f" (!?) *)
     val f = Free ("f", domain_type (fastype_of u));
     val f' = Free ("f'", domain_type (fastype_of u'));
-    val lhs = mk_comp (u $ f) (u' $ f');
+    val lhs = HOLogic.mk_comp (u $ f, u' $ f');
     val rhs =
       if comp
-      then u $ mk_comp f f'
-      else mk_comp (u' $ f') (u $ f);
+      then u $ HOLogic.mk_comp (f, f')
+      else HOLogic.mk_comp (u' $ f', u $ f);
     val prop = lhs === rhs;
     val othm =
       Goal.prove (ProofContext.init_global thy) [] [] prop
diff -r 5895c525739d -r 15b97bd4b5c0 src/HOL/Tools/smallvalue_generators.ML
--- a/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 15:03:44 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 15:35:40 2010 +0100
@@ -18,14 +18,6 @@
 
 (** general term functions **)
 
-fun mk_fun_comp (t, u) =
-  let
-    val (_, B) = dest_funT (fastype_of t)
-    val (C, A) = dest_funT (fastype_of u)
-  in
-    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
-  end;
-
 fun mk_measure f =
   let
     val Type ("fun", [T, @{typ nat}]) = fastype_of f 
@@ -136,7 +128,7 @@
   let
     val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
     val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
-    fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
+    fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
       Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
     fun mk_termination_measure T =
       let