--- a/quotient.ML	Fri Oct 23 18:20:06 2009 +0200
+++ b/quotient.ML	Sat Oct 24 01:33:29 2009 +0200
@@ -1,6 +1,7 @@
 signature QUOTIENT =
 sig
   type maps_info = {mapfun: string, relfun: string}
+  type quotient_info = {qtyp: typ, rtyp: typ, rel: term}
   val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
@@ -8,6 +9,9 @@
   val maps_lookup: theory -> string -> maps_info option
   val maps_update: string -> maps_info -> theory -> theory                                  
   val print_quotdata: Proof.context -> unit
+  val quotdata_lookup: theory -> quotient_info list
+  val quotdata_update_thy: (typ * typ * term) -> theory -> theory
+  val quotdata_update: (typ * typ * term) -> Proof.context -> Proof.context
 end;
 
 structure Quotient: QUOTIENT =
@@ -41,9 +45,11 @@
    fun merge _ = (op @))
 
 val quotdata_lookup = QuotData.get
-fun quotdata_update (qty, rty, rel) = 
+fun quotdata_update_thy (qty, rty, rel) = 
       QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls)
 
+fun quotdata_update (qty, rty, rel) = ProofContext.theory (quotdata_update_thy (qty, rty, rel))
+
 fun print_quotdata ctxt =
 let
   val quots = QuotData.get (ProofContext.theory_of ctxt)
@@ -174,7 +180,7 @@
   val rep = Const (rep_name, abs_ty --> rep_ty)
 
   (* storing the quot-info *)
-  val _ = quotdata_update (abs_ty, rty, rel) (ProofContext.theory_of lthy)
+  (*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 )
@@ -211,11 +217,7 @@
   val mthdt = Method.Basic (fn _ => mthd)
   val bymt = Proof.global_terminal_proof (mthdt, NONE)
   val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
-    Expression.Named [
-     ("R", rel),
-     ("Abs", abs),
-     ("Rep", rep)
-    ]))]
+    Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]
 in
   lthy4
   |> note (quot_thm_name, quot_thm)