--- 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 *)