src/Pure/Syntax/syn_trans.ML
changeset 8575 7d79d2473b5e
parent 8560 2278de8bde59
child 8577 4a3cdf01531b
equal deleted inserted replaced
8574:bed3b994ab26 8575:7d79d2473b5e
   303   | dependent_tr' _ _ = raise Match;
   303   | dependent_tr' _ _ = raise Match;
   304 
   304 
   305 
   305 
   306 (* quote / antiquote *)
   306 (* quote / antiquote *)
   307 
   307 
   308 fun no_loose_bvar i t =
       
   309   if Term.loose_bvar1 (t, i) then raise Match else t;
       
   310 
       
   311 fun quote_antiquote_tr' quoteN antiquoteN name =
   308 fun quote_antiquote_tr' quoteN antiquoteN name =
   312   let
   309   let
   313     fun antiquote_tr' i (t $ u) =
   310     fun antiquote_tr' i (t $ u) =
   314           if u = Bound i then Lexicon.const antiquoteN $ no_loose_bvar i t
   311           if u = Bound i then Lexicon.const antiquoteN $ antiquote_tr' i t
   315           else antiquote_tr' i t $ antiquote_tr' i u
   312           else antiquote_tr' i t $ antiquote_tr' i u
   316       | antiquote_tr' i (Abs (x, T, t)) = Abs (x, T, antiquote_tr' (i + 1) t)
   313       | antiquote_tr' i (Abs (x, T, t)) = Abs (x, T, antiquote_tr' (i + 1) t)
   317       | antiquote_tr' i a = no_loose_bvar i a;
   314       | antiquote_tr' i a = if a = Bound i then raise Match else a;
   318 
   315 
   319     fun quote_tr' (Abs (x, T, t) :: ts) =
   316     fun quote_tr' (Abs (x, T, t) :: ts) =
   320           Term.list_comb (Lexicon.const quoteN $ Term.incr_boundvars ~1 (antiquote_tr' 0 t), ts)
   317           Term.list_comb (Lexicon.const quoteN $ Term.incr_boundvars ~1 (antiquote_tr' 0 t), ts)
   321       | quote_tr' _ = raise Match;
   318       | quote_tr' _ = raise Match;
   322   in (name, quote_tr') end;
   319   in (name, quote_tr') end;