src/Pure/Syntax/syn_ext.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15754 f867c48de2e1
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -144,9 +144,9 @@
     1.4        | del_of _ = NONE;
     1.5  
     1.6      fun dels_of (XProd (_, xsymbs, _, _)) =
     1.7 -      mapfilter del_of xsymbs;
     1.8 +      List.mapPartial del_of xsymbs;
     1.9    in
    1.10 -    map Symbol.explode (distinct (flat (map dels_of xprods)))
    1.11 +    map Symbol.explode (distinct (List.concat (map dels_of xprods)))
    1.12    end;
    1.13  
    1.14  
    1.15 @@ -206,14 +206,14 @@
    1.16      $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
    1.17  
    1.18    val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
    1.19 -  val read_symbs = mapfilter I o the o Scan.read Symbol.stopper scan_symbs;
    1.20 +  val read_symbs = List.mapPartial I o valOf o Scan.read Symbol.stopper scan_symbs;
    1.21  
    1.22    fun unique_index xsymbs =
    1.23 -    if length (filter is_index xsymbs) <= 1 then xsymbs
    1.24 +    if length (List.filter is_index xsymbs) <= 1 then xsymbs
    1.25      else error "Duplicate index arguments (\\<index>)";
    1.26  in
    1.27    val read_mixfix = unique_index o read_symbs o Symbol.explode;
    1.28 -  val mfix_args = length o filter is_argument o read_mixfix;
    1.29 +  val mfix_args = length o List.filter is_argument o read_mixfix;
    1.30    val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
    1.31  end;
    1.32  
    1.33 @@ -261,7 +261,7 @@
    1.34  
    1.35  
    1.36      val raw_symbs = read_mixfix sy handle ERROR => err_in_mfix "" mfix;
    1.37 -    val args = filter (fn Argument _ => true | _ => false) raw_symbs;
    1.38 +    val args = List.filter (fn Argument _ => true | _ => false) raw_symbs;
    1.39      val (const', typ', parse_rules) =
    1.40        if not (exists is_index args) then (const, typ, [])
    1.41        else
    1.42 @@ -293,11 +293,11 @@
    1.43      val symbs' = map (logify_types copy_prod) symbs;
    1.44      val xprod = XProd (lhs', symbs', const', pri);
    1.45  
    1.46 -    val _ = (seq check_pri pris; check_pri pri; check_blocks symbs');
    1.47 +    val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
    1.48      val xprod' =
    1.49        if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
    1.50        else if const <> "" then xprod
    1.51 -      else if length (filter is_argument symbs') <> 1 then
    1.52 +      else if length (List.filter is_argument symbs') <> 1 then
    1.53          err_in_mfix "Copy production must have exactly one argument" mfix
    1.54        else if exists is_terminal symbs' then xprod
    1.55        else XProd (lhs', map rem_pri symbs', "", chain_pri);
    1.56 @@ -330,7 +330,7 @@
    1.57        print_ast_translation) = trfuns;
    1.58  
    1.59      val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
    1.60 -      |> split_list |> apsnd (rev o flat);
    1.61 +      |> split_list |> apsnd (rev o List.concat);
    1.62      val mfix_consts = distinct (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
    1.63    in
    1.64      SynExt {