diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/Syntax/syntax.ML	Thu Apr 27 15:06:35 2006 +0200
@@ -114,8 +114,7 @@
 (** tables of token translation functions **)
 
 fun lookup_tokentr tabs modes =
-  let val trs = distinct (eq_fst (op =))
-    (List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""])))
+  let val trs = distinct (eq_fst (op =)) (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
   in fn c => Option.map fst (AList.lookup (op =) trs c) end;
 
 fun merge_tokentrtabs tabs1 tabs2 =
@@ -150,7 +149,7 @@
 
 type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
 
-fun dest_ruletab tab = List.concat (map snd (Symtab.dest tab));
+fun dest_ruletab tab = maps snd (Symtab.dest tab);
 
 
 (* empty, extend, merge ruletabs *)
@@ -474,8 +473,8 @@
 
 fun prep_rules rd_pat raw_rules =
   let val rules = map (map_trrule rd_pat) raw_rules in
-    (map check_rule (List.mapPartial parse_rule rules),
-      map check_rule (List.mapPartial print_rule rules))
+    (map check_rule (map_filter parse_rule rules),
+      map check_rule (map_filter print_rule rules))
   end
 
 in