--- a/QuotTest.thy	Sun Oct 25 01:31:04 2009 +0200
+++ b/QuotTest.thy	Sun Oct 25 23:44:41 2009 +0100
@@ -13,13 +13,13 @@
 where
   r_eq: "EQUIV RR"
 
-ML {* print_quotdata @{context} *}
+print_quotients
 
 quotient qtrm = trm / "RR"
   apply(rule r_eq)
   done
 
-ML {* print_quotdata @{context} *}
+print_quotients
 
 typ qtrm
 term Rep_qtrm
@@ -51,6 +51,7 @@
   apply(rule r_eq')
   done
 
+print_quotients
 print_theorems
 
 term ABS_qtrm'
@@ -72,6 +73,13 @@
 quotient qt = "t" / "Rt"
   by (rule t_eq)
 
+print_quotients
+
+ML {*
+Toplevel.context_of;
+Toplevel.keep
+*}
+
 ML {*
   get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
   |> fst
@@ -130,6 +138,7 @@
   apply(rule t_eq')
   done
 
+print_quotients
 print_theorems
 
 local_setup {*