--- a/QuotMain.thy	Sat Oct 17 10:40:54 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 12:19:06 2009 +0200
@@ -250,9 +250,13 @@
 
 ML {* lookup @{theory} @{type_name list} *}
 
-term fun_map
 
 ML {*
+(* calculates the aggregate abs and rep functions for a given type; 
+   repF is for constants' arguments; absF is for constants;
+   function types need to be treated specially, since repF and absF
+   change   
+*)
 datatype flag = absF | repF
 
 fun negF absF = repF
@@ -275,18 +279,15 @@
     | NONE      => raise ERROR ("no map association for type " ^ s))
   end
 
-  fun get_fun_fun s fs_tys =
+  fun get_fun_fun fs_tys =
   let
     val (fs, tys) = split_list fs_tys
     val ([oty1, oty2], [nty1, nty2]) = split_list tys
-    val oty = Type (s, [nty1, oty2])
-    val nty = Type (s, [oty1, nty2])
-    val _ = tracing (Syntax.string_of_typ @{context} oty)
+    val oty = Type ("fun", [nty1, oty2])
+    val nty = Type ("fun", [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))
+    (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
   end
 
   fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
@@ -299,19 +300,17 @@
   then (get_const flag)
   else (case ty of
           TFree _ => (mk_identity ty, (ty, ty))
-        | Type (_, []) => (mk_identity ty, (ty, ty))
+        | Type (_, []) => (mk_identity ty, (ty, ty)) 
         | Type ("fun" , [ty1, ty2]) => 
-                 get_fun_fun "fun" [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2]
+                 get_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")
        )
 end
 *}
 
-term fun_map
-
 ML {*
-  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((qt \<Rightarrow> qt) list) * nat"}
+  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
   |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
@@ -320,38 +319,16 @@
 ML {*
   get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}
   |> fst
-  |> type_of
-*}
-
-text {*
-
-Christian:
-
-When "get_fun" gets a function type, it should call itself
-recursively for the right side of the arrow and call itself
-recursively with the flag swapped for left side. This way
-for a simple (qt\<Rightarrow>qt) function type it will make a (REP--->ABS).
-
-Examples of what it should do from Peter's code follow:
-
-- mkabs ``\x : 'a list.x``;
-> val it = ``(finite_set_REP --> finite_set_ABS) (\x. x)`` : term
-- mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``;
-> val it = ``((finite_set_ABS --> finite_set_REP) --> finite_set_ABS) (\x. y)``
-- mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``;
-> val it =
-``(((finite_set_REP --> finite_set_ABS) --> finite_set_REP) -->
-   finite_set_ABS) (\x. y)`` : term
-
-It currently doesn't do it, the following code generates a wrong
-function and the second ML block fails to typecheck for this reason:
-
+  |> Syntax.string_of_term @{context}
+  |> writeln
 *}
 
 ML {*
-    get_fun repF @{typ t} @{typ qt} @{context} @{typ "((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt"}
- |> fst
- |> cterm_of @{theory}
+  get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
+  |> fst
+  |> Syntax.pretty_term @{context}
+  |> Pretty.string_of
+  |> writeln
 *}
 
 text {* produces the definition for a lifted constant *}