# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1257347439 -3600
# Node ID 78bc4d9d7975bfd4a6a921c6db17bf01eff38662
# Parent  5470176d67300792f4767a245ffc858af8d7e182
Two new tests for get_fun. Second one fails.

diff -r 5470176d6730 -r 78bc4d9d7975 QuotTest.thy
--- 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