# HG changeset patch
# User wenzelm
# Date 1415375709 -3600
# Node ID 13d3eb07a17adf70f3a288c151c1016b5283a69b
# Parent  4aa9b3ab0b403971cd07d02964a4c7075f615bb0
tuned signature;

diff -r 4aa9b3ab0b40 -r 13d3eb07a17a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Nov 07 16:51:36 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 07 16:55:09 2014 +0100
@@ -705,11 +705,11 @@
   Outer_Syntax.command @{command_spec "help"}
     "retrieve outer syntax commands according to name patterns"
     (Scan.repeat Parse.name >>
-      (fn pats => Toplevel.keep (fn st => Outer_Syntax.help_syntax (Toplevel.theory_of st) pats)));
+      (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_commands"} "print outer syntax commands"
-    (Scan.succeed (Toplevel.keep (Outer_Syntax.print_syntax o Toplevel.theory_of)));
+    (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.command @{command_spec "print_options"} "print configuration options"
diff -r 4aa9b3ab0b40 -r 13d3eb07a17a src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Nov 07 16:51:36 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Nov 07 16:55:09 2014 +0100
@@ -8,8 +8,8 @@
 sig
   datatype markup = Markup | Markup_Env | Verbatim
   val is_markup: theory -> markup -> string -> bool
-  val help_syntax: theory -> string list -> unit
-  val print_syntax: theory -> unit
+  val help: theory -> string list -> unit
+  val print_commands: theory -> unit
   type command_spec = string * Position.T
   val command: command_spec -> string ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
@@ -114,13 +114,13 @@
   get_syntax #> (fn Syntax {markups, ...} => fn kind => fn name =>
     AList.lookup (op =) markups name = SOME kind);
 
-fun help_syntax thy pats =
+fun help thy pats =
   dest_commands thy
   |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
   |> map pretty_command
   |> Pretty.writeln_chunks;
 
-fun print_syntax thy =
+fun print_commands thy =
   let
     val keywords = Thy_Header.get_keywords thy;
     val minor = Scan.dest_lexicon (Keyword.minor_keywords keywords);