src/HOL/Tools/record.ML

--- a/src/HOL/Tools/record.ML	Wed Dec 01 11:32:24 2010 +0100
+++ b/src/HOL/Tools/record.ML	Wed Dec 01 13:09:08 2010 +0100
@@ -1016,8 +1016,7 @@
 fun mk_comp f g =
   let
     val X = fastype_of g;
-    val A = domain_type X;
-    val B = range_type X;
+    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;