diff -r 2f72662d21f3 -r 54f186bb5e3e Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Tue Dec 22 21:44:50 2009 +0100
+++ b/Quot/quotient_info.ML	Tue Dec 22 22:10:48 2009 +0100
@@ -90,12 +90,10 @@
 let
   fun prt_map (ty_name, {mapfun, relfun}) = 
       Pretty.block (Library.separate (Pretty.brk 2)
-          [Pretty.str "type:", 
-           Pretty.str ty_name,
-           Pretty.str "map fun:", 
-           Pretty.str mapfun,
-           Pretty.str "relation map:", 
-           Pretty.str relfun])
+        (map Pretty.str 
+          ["type:", ty_name,
+           "map fun:", mapfun,
+           "relation map:", relfun]))
 in
   MapsData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest
@@ -104,11 +102,7 @@
   |> Pretty.writeln
 end
 
-val _ = 
-  OuterSyntax.improper_command "print_maps" "prints out all map functions" 
-    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of)))
-
-
+ 
 (* info about quotient types *)
 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
 
@@ -152,10 +146,6 @@
   |> Pretty.writeln
 end
 
-val _ = 
-  OuterSyntax.improper_command "print_quotients" "prints out all quotients" 
-    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
-
 
 (* info about quotient constants *)
 type qconsts_info = {qconst: term, rconst: term, def: thm}
@@ -212,10 +202,6 @@
   |> Pretty.writeln
 end
 
-val _ = 
-  OuterSyntax.improper_command "print_quotconsts" "prints out all quotient constants" 
-    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
-
 (* FIXME/TODO: check the various lemmas conform *)
 (* with the required shape                      *)
 
@@ -257,6 +243,7 @@
 val quotient_rules_add = QuotientRules.add
 
 (* setup of the theorem lists *)
+
 val _ = Context.>> (Context.map_theory 
     (EquivRules.setup #>
      RspRules.setup #>
@@ -264,5 +251,18 @@
      IdSimps.setup #>
      QuotientRules.setup))
 
+
+(* setup of the printing commands *)
+
+fun improper_command (pp_fn, cmd_name, descr_str) =  
+  OuterSyntax.improper_command cmd_name descr_str 
+    OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
+
+val _ = map improper_command 
+         [(print_mapsinfo, "print_maps", "prints out all map functions"),
+          (print_quotinfo, "print_quotients", "prints out all quotients"), 
+          (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
+
+
 end; (* structure *)