--- a/src/HOL/Tools/Quotient/quotient_info.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Mon May 17 23:54:15 2010 +0200
@@ -91,9 +91,9 @@
val maps_attr_parser =
Args.context -- Scan.lift
- ((Args.name --| OuterParse.$$$ "=") --
- (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
- Args.name --| OuterParse.$$$ ")"))
+ ((Args.name --| Parse.$$$ "=") --
+ (Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," --
+ Args.name --| Parse.$$$ ")"))
val _ = Context.>> (Context.map_theory
(Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
@@ -278,8 +278,8 @@
(* 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)))
+ Outer_Syntax.improper_command cmd_name descr_str
+ Keyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
val _ = map improper_command
[(print_mapsinfo, "print_quotmaps", "prints out all map functions"),