1.1 --- a/src/Pure/Syntax/parser.ML	Mon Apr 04 23:26:32 2011 +0200
     1.2 +++ b/src/Pure/Syntax/parser.ML	Mon Apr 04 23:52:56 2011 +0200
     1.3 @@ -706,15 +706,15 @@
     1.4  
     1.5  
     1.6  fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) =
     1.7 -  if Lexicon.valued_token c then (A, j, ts @ [Tip c], sa, id, i)
     1.8 +  if Lexicon.valued_token c then (A, j, Tip c :: ts, sa, id, i)
     1.9    else (A, j, ts, sa, id, i);
    1.10  
    1.11  fun movedot_nonterm tt (A, j, ts, Nonterminal _ :: sa, id, i) =
    1.12 -  (A, j, ts @ tt, sa, id, i);
    1.13 +  (A, j, List.revAppend (tt, ts), sa, id, i);
    1.14  
    1.15  fun movedot_lambda [] _ = []
    1.16    | movedot_lambda ((t, ki) :: ts) (state as (B, j, tss, Nonterminal (A, k) :: sa, id, i)) =
    1.17 -      if k <= ki then (B, j, tss @ t, sa, id, i) :: movedot_lambda ts state
    1.18 +      if k <= ki then (B, j, List.revAppend (t, tss), sa, id, i) :: movedot_lambda ts state
    1.19        else movedot_lambda ts state;
    1.20  
    1.21  
    1.22 @@ -784,7 +784,7 @@
    1.23                  (S :: Si,
    1.24                    if Lexicon.matching_tokens (a, c) then movedot_term c S :: Sii else Sii)
    1.25            | (A, prec, ts, [], id, j) => (*completer operation*)
    1.26 -              let val tt = if id = "" then ts else [Node (id, ts)] in
    1.27 +              let val tt = if id = "" then ts else [Node (id, rev ts)] in
    1.28                  if j = i then (*lambda production?*)
    1.29                    let
    1.30                      val (used', prec') = update_trees used (A, (tt, prec));