--- a/src/Pure/Isar/isar_syn.ML Thu Nov 05 20:44:42 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Thu Nov 05 22:06:46 2009 +0100
@@ -22,8 +22,9 @@
"advanced", "and", "assumes", "attach", "begin", "binder",
"constrains", "defines", "fixes", "for", "identifier", "if",
"imports", "in", "infix", "infixl", "infixr", "is",
- "notes", "obtains", "open", "output", "overloaded", "shows",
- "structure", "unchecked", "uses", "where", "|"];
+ "notes", "obtains", "open", "output", "overloaded", "pervasive",
+ "shows", "structure", "unchecked", "uses", "where", "|"];
+
(** init and exit **)
@@ -337,7 +338,7 @@
val _ =
OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
- (P.ML_source >> IsarCmd.declaration);
+ (P.opt_keyword "pervasive" -- P.ML_source >> uncurry IsarCmd.declaration);
val _ =
OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)