# HG changeset patch
# User wenzelm
# Date 1452953020 -3600
# Node ID d54e916b8b65002396fef1ead632fd6786158228
# Parent  3501964c4908ac8b07170ac274784292b0f86b95
tuned message;

diff -r 3501964c4908 -r d54e916b8b65 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jan 15 19:55:11 2016 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jan 16 15:03:40 2016 +0100
@@ -171,7 +171,7 @@
     ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
 
 val _ =
-  hide_names @{command_keyword hide_const} "constants" Sign.hide_const Parse.const
+  hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const
     ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
 
 val _ =