src/Pure/Isar/rule_insts.ML
changeset 27378 0968c0d0b969
parent 27282 432a5baa7546
child 27809 a1e409db516b
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Sat Jun 28 15:17:24 2008 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat Jun 28 15:17:26 2008 +0200
     1.3 @@ -406,7 +406,7 @@
     1.4  
     1.5  val insts =
     1.6    Scan.optional
     1.7 -    (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
     1.8 +    (Args.and_list1 (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
     1.9        Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
    1.10  
    1.11  fun inst_args f src ctxt =
    1.12 @@ -414,7 +414,7 @@
    1.13  
    1.14  val insts_var =
    1.15    Scan.optional
    1.16 -    (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
    1.17 +    (Args.and_list1 (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
    1.18        Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
    1.19  
    1.20  fun inst_args_var f src ctxt =