src/Pure/Tools/rail.ML
changeset 59058 a78612c67ec0
parent 58978 e42da880c61e
child 59064 a8bcb5a446c8
     1.1 --- a/src/Pure/Tools/rail.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/Pure/Tools/rail.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -265,11 +265,11 @@
     1.4  fun prepare_trees (CAT (ts, _)) = Cat (0, map prepare_tree ts)
     1.5  and prepare_tree (BAR (Ts, _)) = bar (map prepare_trees Ts)
     1.6    | prepare_tree (STAR (Ts, _)) =
     1.7 -      let val (cat1, cat2) = pairself prepare_trees Ts in
     1.8 +      let val (cat1, cat2) = apply2 prepare_trees Ts in
     1.9          if is_empty cat2 then plus (empty, cat1)
    1.10          else bar [empty, cat [plus (cat1, cat2)]]
    1.11        end
    1.12 -  | prepare_tree (PLUS (Ts, _)) = plus (pairself prepare_trees Ts)
    1.13 +  | prepare_tree (PLUS (Ts, _)) = plus (apply2 prepare_trees Ts)
    1.14    | prepare_tree (MAYBE (t, _)) = bar [empty, cat [prepare_tree t]]
    1.15    | prepare_tree (NEWLINE _) = Newline 0
    1.16    | prepare_tree (NONTERMINAL (a, _)) = Nonterminal a