--- a/src/HOL/Tools/BNF/bnf_util.ML Tue Jun 10 19:51:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Tue Jun 10 21:15:57 2014 +0200
@@ -308,9 +308,9 @@
| extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")");
val parse_map_rel_bindings =
- @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"}
- >> (fn ps => fold extract_map_rel ps no_map_rel) ||
- Scan.succeed no_map_rel;
+ @{keyword "for"} |-- Scan.repeat parse_map_rel_binding
+ >> (fn ps => fold extract_map_rel ps no_map_rel)
+ || Scan.succeed no_map_rel;
(*TODO: is this really different from Typedef.add_typedef_global?*)