more standard package setup;
authorwenzelm
Fri Jan 07 21:51:28 2011 +0100 (2011-01-07)
changeset 41452c291e0826902
parent 41451 892e67be8304
child 41453 c03593812297
more standard package setup;
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_info.ML
     1.1 --- a/src/HOL/Quotient.thy	Fri Jan 07 21:26:49 2011 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Fri Jan 07 21:51:28 2011 +0100
     1.3 @@ -667,6 +667,7 @@
     1.4  text {* Auxiliary data for the quotient package *}
     1.5  
     1.6  use "Tools/Quotient/quotient_info.ML"
     1.7 +setup Quotient_Info.setup
     1.8  
     1.9  declare [[map "fun" = (map_fun, fun_rel)]]
    1.10  
     2.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 21:26:49 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 21:51:28 2011 +0100
     2.3 @@ -44,6 +44,7 @@
     2.4    val id_simps_get: Proof.context -> thm list
     2.5    val quotient_rules_get: Proof.context -> thm list
     2.6    val quotient_rules_add: attribute
     2.7 +  val setup: theory -> theory
     2.8  end;
     2.9  
    2.10  structure Quotient_Info: QUOTIENT_INFO =
    2.11 @@ -99,10 +100,6 @@
    2.12        (Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," --
    2.13          Args.name --| Parse.$$$ ")"))
    2.14  
    2.15 -val _ = Context.>> (Context.map_theory
    2.16 -  (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
    2.17 -    "declaration of map information"))
    2.18 -
    2.19  fun print_mapsinfo ctxt =
    2.20    let
    2.21      fun prt_map (ty_name, {mapfun, relmap}) =
    2.22 @@ -284,25 +281,32 @@
    2.23  val quotient_rules_get = QuotientRules.get
    2.24  val quotient_rules_add = QuotientRules.add
    2.25  
    2.26 -(* setup of the theorem lists *)
    2.27 +
    2.28 +(* theory setup *)
    2.29  
    2.30 -val _ = Context.>> (Context.map_theory
    2.31 -  (EquivRules.setup #>
    2.32 -   RspRules.setup #>
    2.33 -   PrsRules.setup #>
    2.34 -   IdSimps.setup #>
    2.35 -   QuotientRules.setup))
    2.36 +val setup =
    2.37 +  Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
    2.38 +    "declaration of map information" #>
    2.39 +  EquivRules.setup #>
    2.40 +  RspRules.setup #>
    2.41 +  PrsRules.setup #>
    2.42 +  IdSimps.setup #>
    2.43 +  QuotientRules.setup
    2.44 +
    2.45  
    2.46 -(* setup of the printing commands *)
    2.47 +(* outer syntax commands *)
    2.48 +
    2.49 +val _ =
    2.50 +  Outer_Syntax.improper_command "print_quotmaps" "print quotient map functions" Keyword.diag
    2.51 +    (Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of)))
    2.52  
    2.53 -fun improper_command (pp_fn, cmd_name, descr_str) =
    2.54 -  Outer_Syntax.improper_command cmd_name descr_str
    2.55 -    Keyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
    2.56 +val _ =
    2.57 +  Outer_Syntax.improper_command "print_quotients" "print quotients" Keyword.diag
    2.58 +    (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
    2.59  
    2.60 -val _ = map improper_command
    2.61 -  [(print_mapsinfo, "print_quotmaps", "print out all map functions"),
    2.62 -   (print_quotinfo, "print_quotients", "print out all quotients"),
    2.63 -   (print_qconstinfo, "print_quotconsts", "print out all quotient constants")]
    2.64 +val _ =
    2.65 +  Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag
    2.66 +    (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
    2.67  
    2.68  
    2.69  end; (* structure *)