--- a/quotient.ML	Sat Oct 24 08:09:40 2009 +0200
+++ b/quotient.ML	Sat Oct 24 08:24:26 2009 +0200
@@ -1,7 +1,6 @@
 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
@@ -9,9 +8,6 @@
   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 =
@@ -45,11 +41,9 @@
    fun merge _ = (op @))
 
 val quotdata_lookup = QuotData.get
-fun quotdata_update_thy (qty, rty, rel) = 
+fun quotdata_update (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)
@@ -180,7 +174,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 )
@@ -217,7 +211,11 @@
   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)