--- a/QuotTest.thy	Wed Nov 04 16:10:39 2009 +0100
+++ b/QuotTest.thy	Thu Nov 05 09:38:34 2009 +0100
@@ -120,25 +120,18 @@
 
 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 {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a ql \<Rightarrow> ?'a ql"})) *}
 
 ML {*
-  get_fun absF [(al, aq)] @{context} ttt
-  |> fst
-  |> Syntax.pretty_term @{context}
-  |> Pretty.string_of
-  |> writeln
+  fst (get_fun absF [(aq, al)] @{context} ttt)
+  |> cterm_of @{theory}
 *}
 
-
-ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat list \<Rightarrow> nat list"})) *}
+ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat ql \<Rightarrow> bool ql \<Rightarrow> 'a ql"})) *}
 
 ML {*
-  get_fun absF [(al, aq)] @{context} ttt2
-  |> fst
-  |> Syntax.pretty_term @{context}
-  |> Pretty.string_of
-  |> writeln
+  fst (get_fun absF [(aq, al), (@{typ "nat ql"}, @{typ "nat list"}), (@{typ "bool ql"}, @{typ "bool list"})] @{context} ttt2)
+  |> cterm_of @{theory}
 *}
 
 quotient_def (for qt)