# HG changeset patch
# User wenzelm
# Date 1294433488 -3600
# Node ID c291e0826902246114b1778720eb238fa3526024
# Parent  892e67be8304926a8283c58bf4b89b0d67858cc5
more standard package setup;

diff -r 892e67be8304 -r c291e0826902 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Jan 07 21:26:49 2011 +0100
+++ b/src/HOL/Quotient.thy	Fri Jan 07 21:51:28 2011 +0100
@@ -667,6 +667,7 @@
 text {* Auxiliary data for the quotient package *}
 
 use "Tools/Quotient/quotient_info.ML"
+setup Quotient_Info.setup
 
 declare [[map "fun" = (map_fun, fun_rel)]]
 
diff -r 892e67be8304 -r c291e0826902 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 21:26:49 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 21:51:28 2011 +0100
@@ -44,6 +44,7 @@
   val id_simps_get: Proof.context -> thm list
   val quotient_rules_get: Proof.context -> thm list
   val quotient_rules_add: attribute
+  val setup: theory -> theory
 end;
 
 structure Quotient_Info: QUOTIENT_INFO =
@@ -99,10 +100,6 @@
       (Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," --
         Args.name --| Parse.$$$ ")"))
 
-val _ = Context.>> (Context.map_theory
-  (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
-    "declaration of map information"))
-
 fun print_mapsinfo ctxt =
   let
     fun prt_map (ty_name, {mapfun, relmap}) =
@@ -284,25 +281,32 @@
 val quotient_rules_get = QuotientRules.get
 val quotient_rules_add = QuotientRules.add
 
-(* setup of the theorem lists *)
+
+(* theory setup *)
 
-val _ = Context.>> (Context.map_theory
-  (EquivRules.setup #>
-   RspRules.setup #>
-   PrsRules.setup #>
-   IdSimps.setup #>
-   QuotientRules.setup))
+val setup =
+  Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
+    "declaration of map information" #>
+  EquivRules.setup #>
+  RspRules.setup #>
+  PrsRules.setup #>
+  IdSimps.setup #>
+  QuotientRules.setup
+
 
-(* setup of the printing commands *)
+(* outer syntax commands *)
+
+val _ =
+  Outer_Syntax.improper_command "print_quotmaps" "print quotient map functions" Keyword.diag
+    (Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of)))
 
-fun improper_command (pp_fn, cmd_name, descr_str) =
-  Outer_Syntax.improper_command cmd_name descr_str
-    Keyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
+val _ =
+  Outer_Syntax.improper_command "print_quotients" "print quotients" Keyword.diag
+    (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
 
-val _ = map improper_command
-  [(print_mapsinfo, "print_quotmaps", "print out all map functions"),
-   (print_quotinfo, "print_quotients", "print out all quotients"),
-   (print_qconstinfo, "print_quotconsts", "print out all quotient constants")]
+val _ =
+  Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag
+    (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
 
 
 end; (* structure *)