--- a/QuotTest.thy Sat Oct 24 17:29:20 2009 +0200
+++ b/QuotTest.thy Sat Oct 24 18:17:38 2009 +0200
@@ -72,7 +72,6 @@
quotient qt = "t" / "Rt"
by (rule t_eq)
-
ML {*
get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
|> fst