tuned;
authorwenzelm
Sat Jun 28 15:17:26 2008 +0200 (2008-06-28 ago)
changeset 273780968c0d0b969
parent 27377 0b9295c598f6
child 27379 c706b7201826
tuned;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/spec_parse.ML
src/Pure/ML/ml_context.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Jun 28 15:17:24 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Jun 28 15:17:26 2008 +0200
     1.3 @@ -572,7 +572,7 @@
     1.4  val _ =
     1.5    OuterSyntax.command "let" "bind text variables"
     1.6      (K.tag_proof K.prf_decl)
     1.7 -    (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term))
     1.8 +    (P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
     1.9        >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind)));
    1.10  
    1.11  val case_spec =
     2.1 --- a/src/Pure/Isar/rule_insts.ML	Sat Jun 28 15:17:24 2008 +0200
     2.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat Jun 28 15:17:26 2008 +0200
     2.3 @@ -406,7 +406,7 @@
     2.4  
     2.5  val insts =
     2.6    Scan.optional
     2.7 -    (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
     2.8 +    (Args.and_list1 (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
     2.9        Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
    2.10  
    2.11  fun inst_args f src ctxt =
    2.12 @@ -414,7 +414,7 @@
    2.13  
    2.14  val insts_var =
    2.15    Scan.optional
    2.16 -    (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
    2.17 +    (Args.and_list1 (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
    2.18        Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
    2.19  
    2.20  fun inst_args_var f src ctxt =
     3.1 --- a/src/Pure/Isar/spec_parse.ML	Sat Jun 28 15:17:24 2008 +0200
     3.2 +++ b/src/Pure/Isar/spec_parse.ML	Sat Jun 28 15:17:26 2008 +0200
     3.3 @@ -56,7 +56,7 @@
     3.4  
     3.5  fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
     3.6  fun opt_thm_name s =
     3.7 -  Scan.optional ((P.name -- opt_attribs || (attribs >> pair "")) --| P.$$$ s) ("", []);
     3.8 +  Scan.optional ((P.name -- opt_attribs || attribs >> pair "") --| P.$$$ s) ("", []);
     3.9  
    3.10  val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
    3.11  val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
     4.1 --- a/src/Pure/ML/ml_context.ML	Sat Jun 28 15:17:24 2008 +0200
     4.2 +++ b/src/Pure/ML/ml_context.ML	Sat Jun 28 15:17:26 2008 +0200
     4.3 @@ -132,10 +132,10 @@
     4.4                NONE => error ("Unknown context -- cannot expand ML antiquotations" ^
     4.5                  Position.str_of pos)
     4.6              | SOME context => Context.proof_of context);
     4.7 -      
     4.8 +
     4.9            val lex = #1 (OuterKeyword.get_lexicons ());
    4.10            fun no_decl _ = ("", "");
    4.11 -      
    4.12 +
    4.13            fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state)
    4.14              | expand (Antiquote.Antiq x) (scope, background) =
    4.15                  let
    4.16 @@ -199,3 +199,4 @@
    4.17  
    4.18  structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
    4.19  open Basic_ML_Context;
    4.20 +