# 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 _ =