tuned message;
authorwenzelm
Sat, 16 Jan 2016 15:03:40 +0100
changeset 62187 d54e916b8b65
parent 62186 3501964c4908
child 62188 74c56f8b68e8
tuned message;
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 _ =