changeset 58893 | 9e0ecb66d6a7 |
parent 57918 | f5d73caba4e5 |
child 58903 | 38c72f5f6c2e |
--- a/src/Pure/Tools/find_consts.ML Mon Nov 03 14:31:15 2014 +0100 +++ b/src/Pure/Tools/find_consts.ML Mon Nov 03 14:50:27 2014 +0100 @@ -149,7 +149,7 @@ |> #1; val _ = - Outer_Syntax.improper_command @{command_spec "find_consts"} + Outer_Syntax.command @{command_spec "find_consts"} "find constants by name / type patterns" (query >> (fn spec => Toplevel.keep (fn st =>