diff -r b054cf6bd179 -r 6ddb2f99be1d QuotMain.thy
--- a/QuotMain.thy	Sun Oct 18 00:52:10 2009 +0200
+++ b/QuotMain.thy	Sun Oct 18 08:44:16 2009 +0200
@@ -284,8 +284,8 @@
   let
     val (fs, tys) = split_list fs_tys
     val ([oty1, oty2], [nty1, nty2]) = split_list tys
-    val oty = Type ("fun", [nty1, oty2])
-    val nty = Type ("fun", [oty1, nty2])
+    val oty = nty1 --> oty2
+    val nty = oty1 --> nty2
     val ftys = map (op -->) tys
   in
     (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))