diff -r f1a840dd0743 -r a0be84b0c707 QuotTest.thy
--- a/QuotTest.thy	Thu Nov 05 10:46:54 2009 +0100
+++ b/QuotTest.thy	Thu Nov 05 13:47:04 2009 +0100
@@ -77,27 +77,19 @@
 print_quotients
 
 ML {*
-Toplevel.context_of;
-Toplevel.keep
-*}
-
-ML {*
   get_fun repF [(@{typ qt}, @{typ qt})] @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
-  |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
 *}
 
 ML {*
   get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "qt * nat"}
-  |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
 *}
 
 ML {*
   get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
-  |> fst
   |> Syntax.pretty_term @{context}
   |> Pretty.string_of
   |> writeln