--- 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
  

--- a/quotient.ML	Thu Oct 22 01:16:42 2009 +0200
+++ b/quotient.ML	Thu Oct 22 01:59:17 2009 +0200
@@ -7,7 +7,7 @@
   val note: binding * thm -> local_theory -> thm * local_theory
   val maps_lookup: theory -> string -> maps_info option
   val maps_update: string -> maps_info -> theory -> theory                                  
-
+  val print_quotdata: Proof.context -> unit
 end;
 
 structure Quotient: QUOTIENT =
@@ -30,7 +30,6 @@
 fun maps_update k v = MapsData.map (Symtab.update (k, v))
 
 
-
 (* info about the quotient types *)
 type quotient_info = {qtyp: typ, rtyp: typ, rel: term}
 
@@ -47,15 +46,12 @@
 
 fun print_quotdata ctxt =
 let
-  val quots = QuotData.get (Context.theory_of_proof ctxt)
-  fun prt_quot {qtyp, rtyp, rel} = Pretty.block
-      [Pretty.str ("quotient:"), 
-       Pretty.brk 2, 
-       Syntax.pretty_typ ctxt qtyp,
-       Pretty.brk 2, 
-       Syntax.pretty_typ ctxt rtyp,
-       Pretty.brk 2, 
-       Syntax.pretty_term ctxt rel]
+  val quots = QuotData.get (ProofContext.theory_of ctxt)
+  fun prt_quot {qtyp, rtyp, rel} = 
+      Pretty.block [Pretty.str ("quotient:"), 
+                    Pretty.brk 2, Syntax.pretty_typ ctxt qtyp,
+                    Pretty.brk 2, Syntax.pretty_typ ctxt rtyp,
+                    Pretty.brk 2, Syntax.pretty_term ctxt rel]
 in
   [Pretty.big_list "quotients:" (map prt_quot quots)]
   |> Pretty.chunks |> Pretty.writeln
@@ -177,6 +173,9 @@
   val abs = Const (abs_name, rep_ty --> abs_ty)
   val rep = Const (rep_name, abs_ty --> rep_ty)
 
+  (* storing the quot-info *)
+  val _ = quotdata_update (abs_ty, rty, rel) (ProofContext.theory_of lthy)
+
   (* ABS and REP definitions *)
   val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
   val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
@@ -246,7 +245,7 @@
 let
   fun get_goal (rty, rel) =
   let
-      val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+    val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   in 
     (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), [])
   end
@@ -274,7 +273,7 @@
     val rel = Syntax.parse_term lthy rel_str
               |> Syntax.check_term lthy
   in
-     ((qty_name, mx), (rty, rel))
+    ((qty_name, mx), (rty, rel))
   end
 in
   mk_quotient_type (map parse_spec spec) lthy