suppress completion of obscure keyword, avoid confusion with plain "simp";
authorwenzelm
Wed, 26 Feb 2014 10:45:06 +0100
changeset 55762 27a45aec67a0
parent 55761 213b9811f59f
child 55763 4b3907cb5654
suppress completion of obscure keyword, avoid confusion with plain "simp";
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