--- a/QuotTest.thy	Wed Nov 04 15:27:32 2009 +0100
+++ b/QuotTest.thy	Wed Nov 04 16:10:39 2009 +0100
@@ -112,6 +112,35 @@
 *}
 *)
 
+consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+axioms Rl_eq: "EQUIV Rl"
+
+quotient ql = "'a list" / "Rl"
+  by (rule Rl_eq)
+
+ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *}
+ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *}
+ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a list \<Rightarrow> ?'a list"})) *}
+
+ML {*
+  get_fun absF [(al, aq)] @{context} ttt
+  |> fst
+  |> Syntax.pretty_term @{context}
+  |> Pretty.string_of
+  |> writeln
+*}
+
+
+ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat list \<Rightarrow> nat list"})) *}
+
+ML {*
+  get_fun absF [(al, aq)] @{context} ttt2
+  |> fst
+  |> Syntax.pretty_term @{context}
+  |> Pretty.string_of
+  |> writeln
+*}
+
 quotient_def (for qt)
   VR ::"string \<Rightarrow> qt"
 where