--- a/quotient.ML	Mon Nov 02 18:16:19 2009 +0100
+++ b/quotient.ML	Mon Nov 02 18:26:55 2009 +0100
@@ -1,112 +1,14 @@
 signature QUOTIENT =
 sig
-  type maps_info = {mapfun: string, relfun: string}
-  type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
   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
   val note: binding * thm -> local_theory -> thm * local_theory
-  val maps_lookup: theory -> string -> maps_info option
-  val maps_update_thy: string -> maps_info -> theory -> theory    
-  val maps_update: string -> maps_info -> Proof.context -> Proof.context                           
-  val print_quotdata: Proof.context -> unit
-  val quotdata_lookup_thy: theory -> quotient_info list
-  val quotdata_lookup: Proof.context -> quotient_info list
-  val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory
-  val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context
 end;
 
 structure Quotient: QUOTIENT =
 struct
 
-(* data containers *)
-(*******************)
-
-(* info about map- and rel-functions *)
-type maps_info = {mapfun: string, relfun: string}
-
-structure MapsData = TheoryDataFun
-  (type T = maps_info Symtab.table
-   val empty = Symtab.empty
-   val copy = I
-   val extend = I
-   fun merge _ = Symtab.merge (K true))
-
-val maps_lookup = Symtab.lookup o MapsData.get
-
-
-fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
-fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
-
-fun maps_attribute_aux s minfo = Thm.declaration_attribute 
-  (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
-
-(* attribute to be used in declare statements *)
-fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = 
-let  
-  val thy = ProofContext.theory_of ctxt
-  val tyname = Sign.intern_type thy tystr
-  val mapname = Sign.intern_const thy mapstr
-  val relname = Sign.intern_const thy relstr
-in
-  maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
-end
-
-val maps_attr_parser = 
-      Args.context -- Scan.lift
-       ((Args.name --| OuterParse.$$$ "=") -- 
-         (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- 
-           Args.name --| OuterParse.$$$ ")"))
-
-val _ = Context.>> (Context.map_theory
-         (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) 
-           "declaration of map information"))
-
-
-(* info about the quotient types *)
-type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
-
-structure QuotData = TheoryDataFun
-  (type T = quotient_info list
-   val empty = []
-   val copy = I
-   val extend = I
-   fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *)
-
-val quotdata_lookup_thy = QuotData.get
-val quotdata_lookup = QuotData.get o ProofContext.theory_of
-
-fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = 
-      QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy
-
-fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = 
-      ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt
-
-fun print_quotdata ctxt =
-let
-  fun prt_quot {qtyp, rtyp, rel, equiv_thm} = 
-      Pretty.block (Library.separate (Pretty.brk 2)
-          [Pretty.str ("quotient type:"), 
-           Syntax.pretty_typ ctxt qtyp,
-           Pretty.str ("raw type:"), 
-           Syntax.pretty_typ ctxt rtyp,
-           Pretty.str ("relation:"), 
-           Syntax.pretty_term ctxt rel,
-           Pretty.str ("equiv. thm:"), 
-           Syntax.pretty_term ctxt (prop_of equiv_thm)])
-in
-  QuotData.get (ProofContext.theory_of ctxt)
-  |> map prt_quot
-  |> Pretty.big_list "quotients:" 
-  |> Pretty.writeln
-end
-
-val _ = 
-  OuterSyntax.improper_command "print_quotients" "print out all quotients" 
-    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of)))
-
-
-
 (* wrappers for define, note and theorem_i *)
 fun define (name, mx, rhs) lthy =
 let