# HG changeset patch
# User wenzelm
# Date 1301131517 -3600
# Node ID 532b3a76103fe8e5258768d0ca5c12c0fc721dd6
# Parent  e1209fc7ecdcf926d0ce156e2d434e594a82f4c8
dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;

diff -r e1209fc7ecdc -r 532b3a76103f src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Thu Mar 24 16:56:19 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Sat Mar 26 10:25:17 2011 +0100
@@ -435,7 +435,7 @@
       if Term.is_dependent B then
         let val (x', B') = variant_abs' (x, dummyT, B);
         in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end
-      else Term.list_comb (Lexicon.const r $ A $ B, ts)  (* FIXME decr!? *)
+      else Term.list_comb (Lexicon.const r $ A $ incr_boundvars ~1 B, ts)
   | dependent_tr' _ _ = raise Match;
 
 
@@ -444,8 +444,8 @@
 fun antiquote_tr' name =
   let
     fun tr' i (t $ u) =
-      if u aconv Bound i then Lexicon.const name $ tr' i t
-      else tr' i t $ tr' i u
+          if u aconv Bound i then Lexicon.const name $ tr' i t
+          else tr' i t $ tr' i u
       | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
       | tr' i a = if a aconv Bound i then raise Match else a;
   in tr' 0 end;