diff -r b1247c98abb8 -r fcacca9588b4 QuotMain.thy
--- a/QuotMain.thy	Sat Oct 24 17:29:20 2009 +0200
+++ b/QuotMain.thy	Sat Oct 24 18:17:38 2009 +0200
@@ -243,6 +243,7 @@
 end
 *}
 
+
 text {* produces the definition for a lifted constant *}
 
 ML {*
@@ -258,11 +259,12 @@
   val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys
   val abs_fn  = (fst o get_fun absF rty qty lthy) res_ty
 
+  fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2
+
+  val fns = Library.foldr (mk_fun_map) (rep_fns, abs_fn)
+            |> Syntax.check_term lthy
 in
-  map (op $) (rep_fns ~~ fresh_args)
-  |> curry list_comb oconst
-  |> curry (op $) abs_fn
-  |> fold_rev lambda fresh_args
+  fns $ oconst
 end
 *}