# HG changeset patch
# User wenzelm
# Date 1214659046 -7200
# Node ID 0968c0d0b96938d9648bbb82b4a0769304f6c1e6
# Parent  0b9295c598f6f7dcfbccc826657dfe2969376743
tuned;

diff -r 0b9295c598f6 -r 0968c0d0b969 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Jun 28 15:17:24 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jun 28 15:17:26 2008 +0200
@@ -572,7 +572,7 @@
 val _ =
   OuterSyntax.command "let" "bind text variables"
     (K.tag_proof K.prf_decl)
-    (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term))
+    (P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
       >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind)));
 
 val case_spec =
diff -r 0b9295c598f6 -r 0968c0d0b969 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Sat Jun 28 15:17:24 2008 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Sat Jun 28 15:17:26 2008 +0200
@@ -406,7 +406,7 @@
 
 val insts =
   Scan.optional
-    (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
+    (Args.and_list1 (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
       Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
 
 fun inst_args f src ctxt =
@@ -414,7 +414,7 @@
 
 val insts_var =
   Scan.optional
-    (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
+    (Args.and_list1 (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
       Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
 
 fun inst_args_var f src ctxt =
diff -r 0b9295c598f6 -r 0968c0d0b969 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Sat Jun 28 15:17:24 2008 +0200
+++ b/src/Pure/Isar/spec_parse.ML	Sat Jun 28 15:17:26 2008 +0200
@@ -56,7 +56,7 @@
 
 fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
 fun opt_thm_name s =
-  Scan.optional ((P.name -- opt_attribs || (attribs >> pair "")) --| P.$$$ s) ("", []);
+  Scan.optional ((P.name -- opt_attribs || attribs >> pair "") --| P.$$$ s) ("", []);
 
 val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
 val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
diff -r 0b9295c598f6 -r 0968c0d0b969 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sat Jun 28 15:17:24 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Sat Jun 28 15:17:26 2008 +0200
@@ -132,10 +132,10 @@
               NONE => error ("Unknown context -- cannot expand ML antiquotations" ^
                 Position.str_of pos)
             | SOME context => Context.proof_of context);
-      
+
           val lex = #1 (OuterKeyword.get_lexicons ());
           fun no_decl _ = ("", "");
-      
+
           fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state)
             | expand (Antiquote.Antiq x) (scope, background) =
                 let
@@ -199,3 +199,4 @@
 
 structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
 open Basic_ML_Context;
+