1.1 --- a/src/Pure/Syntax/syntax.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -114,8 +114,7 @@
     1.4  (** tables of token translation functions **)
     1.5  
     1.6  fun lookup_tokentr tabs modes =
     1.7 -  let val trs = distinct (eq_fst (op =))
     1.8 -    (List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""])))
     1.9 +  let val trs = distinct (eq_fst (op =)) (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
    1.10    in fn c => Option.map fst (AList.lookup (op =) trs c) end;
    1.11  
    1.12  fun merge_tokentrtabs tabs1 tabs2 =
    1.13 @@ -150,7 +149,7 @@
    1.14  
    1.15  type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
    1.16  
    1.17 -fun dest_ruletab tab = List.concat (map snd (Symtab.dest tab));
    1.18 +fun dest_ruletab tab = maps snd (Symtab.dest tab);
    1.19  
    1.20  
    1.21  (* empty, extend, merge ruletabs *)
    1.22 @@ -474,8 +473,8 @@
    1.23  
    1.24  fun prep_rules rd_pat raw_rules =
    1.25    let val rules = map (map_trrule rd_pat) raw_rules in
    1.26 -    (map check_rule (List.mapPartial parse_rule rules),
    1.27 -      map check_rule (List.mapPartial print_rule rules))
    1.28 +    (map check_rule (map_filter parse_rule rules),
    1.29 +      map check_rule (map_filter print_rule rules))
    1.30    end
    1.31  
    1.32  in