--- a/src/HOL/HOLCF/Tools/fixrec.ML Thu Mar 22 21:43:26 2012 +0100
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Fri Mar 23 20:32:43 2012 +0100
@@ -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)"
--- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Mar 22 21:43:26 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 23 20:32:43 2012 +0100
@@ -71,7 +71,7 @@
val quotmaps_attribute_setup =
Attrib.setup @{binding map}
- ((Args.type_name true --| Scan.lift (@{keyword "="})) -- Args.const_proper true >>
+ ((Args.type_name true --| Scan.lift @{keyword "="}) -- Args.const_proper true >>
(fn (tyname, relname) =>
let val minfo = {relmap = relname}
in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
--- a/src/Tools/Code/code_target.ML Thu Mar 22 21:43:26 2012 +0100
+++ b/src/Tools/Code/code_target.ML Fri Mar 23 20:32:43 2012 +0100
@@ -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);