# HG changeset patch # User wenzelm # Date 953807290 -3600 # Node ID 2278de8bde59be15446142b5b6a932bef3d668c9 # Parent fd37531882325c245e84b278110587607e776046 tuned spacing; diff -r fd3753188232 -r 2278de8bde59 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Thu Mar 23 11:27:52 2000 +0100 +++ b/src/Pure/Syntax/syn_trans.ML Thu Mar 23 11:28:10 2000 +0100 @@ -317,7 +317,7 @@ | 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;