1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Mon Mar 26 11:01:04 2012 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon Mar 26 11:15:41 2012 +0200
     1.3 @@ -399,7 +399,7 @@
     1.4  
     1.5  val alt_specs' : (bool * (Attrib.binding * string)) list parser =
     1.6    let val unexpected = Scan.ahead (Parse.name || @{keyword "["} || @{keyword "("})
     1.7 -  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end
     1.8 +  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! @{keyword "|"})) end
     1.9  
    1.10  val _ =
    1.11    Outer_Syntax.local_theory @{command_spec "fixrec"} "define recursive functions (HOLCF)"

     2.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Mon Mar 26 11:01:04 2012 +0200
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Mon Mar 26 11:15:41 2012 +0200
     2.3 @@ -71,9 +71,9 @@
     2.4  
     2.5  val quotmaps_attribute_setup =
     2.6    Attrib.setup @{binding map}
     2.7 -    ((Args.type_name true --| Scan.lift (@{keyword "="})) --
     2.8 -      (Scan.lift (@{keyword "("}) |-- Args.const_proper true --| Scan.lift (@{keyword ","}) --
     2.9 -        Attrib.thm --| Scan.lift (@{keyword ")"})) >>
    2.10 +    ((Args.type_name true --| Scan.lift @{keyword "="}) --
    2.11 +      (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
    2.12 +        Attrib.thm --| Scan.lift @{keyword ")"}) >>
    2.13        (fn (tyname, (relname, qthm)) =>
    2.14          let val minfo = {relmap = relname, quot_thm = qthm}
    2.15          in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))

     3.1 --- a/src/Tools/Code/code_target.ML	Mon Mar 26 11:01:04 2012 +0200
     3.2 +++ b/src/Tools/Code/code_target.ML	Mon Mar 26 11:15:41 2012 +0200
     3.3 @@ -639,7 +639,7 @@
     3.4  fun process_multi_syntax parse_thing parse_syntax change =
     3.5    (Parse.and_list1 parse_thing
     3.6    :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name --
     3.7 -        (zip_list things parse_syntax (@{keyword "and"})) --| @{keyword ")"})))
     3.8 +        (zip_list things parse_syntax @{keyword "and"}) --| @{keyword ")"})))
     3.9    >> (Toplevel.theory oo fold)
    3.10      (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
    3.11