# HG changeset patch
# User wenzelm
# Date 1393407906 -3600
# Node ID 27a45aec67a0d67fee54e58e52ab7df3404e5072
# Parent  213b9811f59f41305877ec807fb939cbda744d74
suppress completion of obscure keyword, avoid confusion with plain "simp";

diff -r 213b9811f59f -r 27a45aec67a0 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Feb 26 10:40:13 2014 +0100
+++ b/src/Pure/Pure.thy	Wed Feb 26 10:45:06 2014 +0100
@@ -33,8 +33,9 @@
   and "ML" :: thy_decl % "ML"
   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
   and "ML_val" "ML_command" :: diag % "ML"
+  and "simproc_setup" :: thy_decl % "ML" == ""
   and "setup" "local_setup" "attribute_setup" "method_setup"
-    "declaration" "syntax_declaration" "simproc_setup"
+    "declaration" "syntax_declaration"
     "parse_ast_translation" "parse_translation" "print_translation"
     "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
   and "bundle" :: thy_decl