# HG changeset patch
# User wenzelm
# Date 1149638492 -7200
# Node ID b8f35de1c664677b3bcb9fde1f6c45a43dc9e01b
# Parent  396dd23c54ef84e0b5a8185e834ab82e441e2667
added 'if' and 'for' keywords;
tuned;

diff -r 396dd23c54ef -r b8f35de1c664 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jun 07 02:01:31 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jun 07 02:01:32 2006 +0200
@@ -356,22 +356,19 @@
       >> (Toplevel.theory_context o (fn ((is_open, name), (expr, elems)) =>
              Locale.add_locale is_open name expr elems #> (fn ((_, ctxt), thy) => (ctxt, thy)))));
 
-val opt_inst =
-  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [];
-
 val interpretationP =
   OuterSyntax.command "interpretation"
     "prove and register interpretation of locale expression in theory or locale" K.thy_goal
     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! P.locale_expr
       >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale)) ||
-     P.opt_thm_name ":" -- P.locale_expr -- opt_inst >> (fn ((x, y), z) =>
+     P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) =>
       Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation x y z)));
 
 val interpretP =
   OuterSyntax.command "interpret"
     "prove and register interpretation of locale expression in proof context"
     (K.tag_proof K.prf_goal)
-    (P.opt_thm_name ":" -- P.locale_expr -- opt_inst >> (fn ((x, y), z) =>
+    (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) =>
       Toplevel.print o Toplevel.proof' (Locale.interpret x y z)));
 
 
@@ -879,9 +876,9 @@
 val _ = OuterSyntax.add_keywords
  ["!", "!!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
   "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes",
-  "begin", "binder", "concl", "constrains", "defines", "fixes",
-  "imports", "in", "includes", "infix", "infixl", "infixr", "is",
-  "notes", "obtains", "open", "output", "overloaded", "shows",
+  "begin", "binder", "concl", "constrains", "defines", "fixes", "for",
+  "imports", "if", "in", "includes", "infix", "infixl", "infixr",
+  "is", "notes", "obtains", "open", "output", "overloaded", "shows",
   "structure", "unchecked", "uses", "where", "|", "\\<equiv>",
   "\\<leftharpoondown>", "\\<rightharpoonup>",
   "\\<rightleftharpoons>", "\\<subseteq>"];