diff -r 48e01d16dd17 -r 2f97215e79bf 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;