src/Pure/Syntax/syntax.ML

 
 
 (** 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 =
   let
     fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;

 
 (** tables of translation rules **)
 
 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 *)
 
 val extend_ruletab = fold_rev (fn r => Symtab.update_list (Ast.head_of_rule r, r));

     cat_error msg ("The error(s) above occurred in translation pattern " ^
       quote str);
 
 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
 
 val cert_rules = prep_rules I;