diff -r 31509c8cf72e -r bdbb52979790 quotient_info.ML
--- a/quotient_info.ML	Sat Nov 21 03:12:50 2009 +0100
+++ b/quotient_info.ML	Sat Nov 21 10:58:08 2009 +0100
@@ -45,6 +45,7 @@
 
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
+(* FIXME: this should be done using a generic context *)
 
 fun maps_attribute_aux s minfo = Thm.declaration_attribute 
   (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
@@ -95,13 +96,13 @@
 let
   fun prt_quot {qtyp, rtyp, rel, equiv_thm} = 
       Pretty.block (Library.separate (Pretty.brk 2)
-          [Pretty.str ("quotient type:"), 
+          [Pretty.str "quotient type:", 
            Syntax.pretty_typ ctxt qtyp,
-           Pretty.str ("raw type:"), 
+           Pretty.str "raw type:", 
            Syntax.pretty_typ ctxt rtyp,
-           Pretty.str ("relation:"), 
+           Pretty.str "relation:", 
            Syntax.pretty_term ctxt rel,
-           Pretty.str ("equiv. thm:"), 
+           Pretty.str "equiv. thm:", 
            Syntax.pretty_term ctxt (prop_of equiv_thm)])
 in
   QuotData.get (ProofContext.theory_of ctxt)
@@ -148,8 +149,7 @@
 val qconsts_lookup = Symtab.lookup o QConstsData.get
 
 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
-fun qconsts_update_gen k qcinfo = 
-      Context.mapping (qconsts_update_thy k qcinfo) I
+fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I
 
 fun print_qconstinfo ctxt =
 let
@@ -170,7 +170,6 @@
   OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
 
-
 end; (* structure *)
 
 open Quotient_Info