--- a/QuotMain.thy	Fri Oct 16 03:26:54 2009 +0200
+++ b/QuotMain.thy	Fri Oct 16 08:48:56 2009 +0200
@@ -250,6 +250,8 @@
 
 ML {* lookup @{theory} @{type_name list} *}
 
+term fun_map
+
 ML {*
 datatype flag = absF | repF
 
@@ -269,6 +271,19 @@
     val ftys = map (op -->) tys
   in
    (case (lookup (ProofContext.theory_of lthy) s) of
+      SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
+    | NONE      => raise ERROR ("no map association for type " ^ s))
+  end
+
+  fun get_fun_fun s fs_tys =
+  let
+    val (fs, tys) = split_list fs_tys
+    val ([oty1, oty2], [nty1, nty2]) = split_list tys
+    val oty = Type (s, [oty2, nty1])
+    val nty = Type (s, [oty1, nty2])
+    val ftys = map (op -->) tys
+  in
+   (case (lookup (ProofContext.theory_of lthy) s) of
       SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))
     | NONE      => raise ERROR ("no map association for type " ^ s))
   end
@@ -285,7 +300,7 @@
           TFree _ => (mk_identity ty, (ty, ty))
         | Type (_, []) => (mk_identity ty, (ty, ty))
         | Type ("fun" , [ty1, ty2]) => 
-                 get_fun_aux "fun" [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2]
+                 get_fun_fun "fun" [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2]
         | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys)
         | _ => raise ERROR ("no type variables")
        )
@@ -302,8 +317,7 @@
 ML {*
   get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}
   |> fst
-  |> Syntax.string_of_term @{context}
-  |> writeln
+  |> type_of
 *}
 
 text {*
@@ -331,7 +345,7 @@
 
 *}
 
-ML {*
+(*ML {*
     get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
  |> fst
  |> type_of
@@ -341,9 +355,9 @@
 ML {*
     get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
  |> fst
- |> Syntax.string_of_term @{context}
- |> writeln
+ |> cterm_of @{theory}
 *}
+*)
 
 ML {*
     get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"}