src/Pure/Syntax/syn_trans.ML

           else antiquote_tr' i t $ antiquote_tr' i u
       | antiquote_tr' i (Abs (x, T, t)) = Abs (x, T, antiquote_tr' (i + 1) t)
       | antiquote_tr' i a = no_loose_bvar i a;
 
     fun quote_tr' (Abs (x, T, t) :: ts) =
-          Term.list_comb ( Lexicon.const quoteN $ Term.incr_boundvars ~1 (antiquote_tr' 0 t), ts)
+          Term.list_comb (Lexicon.const quoteN $ Term.incr_boundvars ~1 (antiquote_tr' 0 t), ts)
       | quote_tr' _ = raise Match;
   in (name, quote_tr') end;