# HG changeset patch
# User wenzelm
# Date 1332753341 -7200
# Node ID 8493d5d0e9b6bf38b87312b2a96ac59c4e4767ad
# Parent  a4476e55a2414c6ed4971bdf95ae2a0aa4aa1fe5# Parent  f067afe98049e4ca183ecb00774a16e2ef52505b
merged

diff -r a4476e55a241 -r 8493d5d0e9b6 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Mon Mar 26 11:01:04 2012 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon Mar 26 11:15:41 2012 +0200
@@ -399,7 +399,7 @@
 
 val alt_specs' : (bool * (Attrib.binding * string)) list parser =
   let val unexpected = Scan.ahead (Parse.name || @{keyword "["} || @{keyword "("})
-  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end
+  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! @{keyword "|"})) end
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "fixrec"} "define recursive functions (HOLCF)"
diff -r a4476e55a241 -r 8493d5d0e9b6 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Mon Mar 26 11:01:04 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Mon Mar 26 11:15:41 2012 +0200
@@ -71,9 +71,9 @@
 
 val quotmaps_attribute_setup =
   Attrib.setup @{binding map}
-    ((Args.type_name true --| Scan.lift (@{keyword "="})) --
-      (Scan.lift (@{keyword "("}) |-- Args.const_proper true --| Scan.lift (@{keyword ","}) --
-        Attrib.thm --| Scan.lift (@{keyword ")"})) >>
+    ((Args.type_name true --| Scan.lift @{keyword "="}) --
+      (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
+        Attrib.thm --| Scan.lift @{keyword ")"}) >>
       (fn (tyname, (relname, qthm)) =>
         let val minfo = {relmap = relname, quot_thm = qthm}
         in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
diff -r a4476e55a241 -r 8493d5d0e9b6 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Mar 26 11:01:04 2012 +0200
+++ b/src/Tools/Code/code_target.ML	Mon Mar 26 11:15:41 2012 +0200
@@ -639,7 +639,7 @@
 fun process_multi_syntax parse_thing parse_syntax change =
   (Parse.and_list1 parse_thing
   :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name --
-        (zip_list things parse_syntax (@{keyword "and"})) --| @{keyword ")"})))
+        (zip_list things parse_syntax @{keyword "and"}) --| @{keyword ")"})))
   >> (Toplevel.theory oo fold)
     (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);