--- a/QuotMain.thy	Thu Oct 22 01:16:42 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 01:59:17 2009 +0200
@@ -3,6 +3,8 @@
 uses ("quotient.ML")
 begin
 
+ML {* Pretty.writeln *}
+ML {*  LocalTheory.theory_result *}
 
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -176,10 +178,14 @@
 where
   r_eq: "EQUIV RR"
 
+ML {* print_quotdata @{context} *}
+
 quotient qtrm = trm / "RR"
   apply(rule r_eq)
   done
 
+ML {* print_quotdata @{context} *}
+
 typ qtrm
 term Rep_qtrm
 term REP_qtrm
@@ -1418,5 +1424,8 @@
 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
 *)
 
+
+
+
 end