diff -r b1247c98abb8 -r fcacca9588b4 QuotTest.thy --- 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 \ qt) \ qt) \ qt) list) * nat"} |> fst