diff -r 3300260b63a1 -r 3413aa899aa7 FSet.thy
--- a/FSet.thy	Sat Oct 24 08:09:09 2009 +0200
+++ b/FSet.thy	Sat Oct 24 08:09:40 2009 +0200
@@ -2,6 +2,49 @@
 imports QuotMain
 begin
 
+(* test for get_fun *)
+datatype t =
+   vr "string"
+ | ap "t list"
+ | lm "string" "t"
+
+consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
+axioms t_eq: "EQUIV Rt"
+
+quotient qt = "t" / "Rt"
+    by (rule t_eq)
+
+setup {*
+  maps_update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>
+  maps_update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
+  maps_update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
+*}
+
+
+ML {*
+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
+*}
+
+ML {*
+get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}
+ |> fst
+ |> Syntax.string_of_term @{context}
+ |> writeln
+*}
+
+ML {*
+get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
+ |> fst
+ |> Syntax.pretty_term @{context}
+ |> Pretty.string_of
+ |> writeln
+*}
+(* end test get_fun *)
+
+
 inductive
   list_eq (infix "\<approx>" 50)
 where