# HG changeset patch
# User wenzelm
# Date 1302262276 -7200
# Node ID 326f57825e1ad06c35028fb0d3d3068b9d556b32
# Parent  25d9d836ed9c47ed13bf626244b27f8c2d4b37d2
explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

diff -r 25d9d836ed9c -r 326f57825e1a NEWS
--- a/NEWS	Fri Apr 08 11:39:45 2011 +0200
+++ b/NEWS	Fri Apr 08 13:31:16 2011 +0200
@@ -93,9 +93,10 @@
 be disabled via the configuration option Syntax.positions, which is
 called "syntax_positions" in Isar attribute syntax.
 
-* Discontinued special treatment of structure Ast: no pervasive
-content, no inclusion in structure Syntax.  INCOMPATIBILITY, refer to
-qualified names like Ast.Constant etc.
+* Discontinued special treatment of various ML structures of inner
+syntax, such as structure Ast: no pervasive content, no inclusion in
+structure Syntax.  INCOMPATIBILITY, refer to qualified names like
+Ast.Constant etc.
 
 * Typed print translation: discontinued show_sorts argument, which is
 already available via context of "advanced" translation.
diff -r 25d9d836ed9c -r 326f57825e1a src/CCL/Term.thy
--- a/src/CCL/Term.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/CCL/Term.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -56,11 +56,11 @@
 (** Quantifier translations: variable binding **)
 
 (* FIXME does not handle "_idtdummy" *)
-(* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
+(* FIXME should use Syntax_Trans.mark_bound(T), Syntax_Trans.variant_abs' *)
 
 fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b);
 fun let_tr' [a,Abs(id,T,b)] =
-     let val (id',b') = variant_abs(id,T,b)
+     let val (id',b') = Syntax_Trans.variant_abs(id,T,b)
      in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
 
 fun letrec_tr [Free(f,S),Free(x,T),a,b] =
@@ -72,23 +72,23 @@
         absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
 
 fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
-     let val (f',b')  = variant_abs(ff,SS,b)
-         val (_,a'') = variant_abs(f,S,a)
-         val (x',a')  = variant_abs(x,T,a'')
+     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
+         val (_,a'') = Syntax_Trans.variant_abs(f,S,a)
+         val (x',a') = Syntax_Trans.variant_abs(x,T,a'')
      in Const(@{syntax_const "_letrec"},dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
 fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
-     let val (f',b') = variant_abs(ff,SS,b)
-         val ( _,a1) = variant_abs(f,S,a)
-         val (y',a2) = variant_abs(y,U,a1)
-         val (x',a') = variant_abs(x,T,a2)
+     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
+         val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
+         val (y',a2) = Syntax_Trans.variant_abs(y,U,a1)
+         val (x',a') = Syntax_Trans.variant_abs(x,T,a2)
      in Const(@{syntax_const "_letrec2"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
       end;
 fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
-     let val (f',b') = variant_abs(ff,SS,b)
-         val ( _,a1) = variant_abs(f,S,a)
-         val (z',a2) = variant_abs(z,V,a1)
-         val (y',a3) = variant_abs(y,U,a2)
-         val (x',a') = variant_abs(x,T,a3)
+     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
+         val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
+         val (z',a2) = Syntax_Trans.variant_abs(z,V,a1)
+         val (y',a3) = Syntax_Trans.variant_abs(y,U,a2)
+         val (x',a') = Syntax_Trans.variant_abs(x,T,a3)
      in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
       end;
 
diff -r 25d9d836ed9c -r 326f57825e1a src/CCL/Type.thy
--- a/src/CCL/Type.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/CCL/Type.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -46,8 +46,10 @@
   "{x: A. B}"   == "CONST Subtype(A, %x. B)"
 
 print_translation {*
- [(@{const_syntax Pi}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
-  (@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
+ [(@{const_syntax Pi},
+    Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
+  (@{const_syntax Sigma},
+    Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
 *}
 
 defs
diff -r 25d9d836ed9c -r 326f57825e1a src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Cube/Cube.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -53,7 +53,8 @@
   "_arrow" :: "[term, term] => term"    (infixr "\<rightarrow>" 10)
 
 print_translation {*
-  [(@{const_syntax Prod}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
+  [(@{const_syntax Prod},
+    Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
 *}
 
 axioms
diff -r 25d9d836ed9c -r 326f57825e1a src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/FOLP/simp.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -371,7 +371,7 @@
 (*Replace parameters by Free variables in P*)
 fun variants_abs ([],P) = P
   | variants_abs ((a,T)::aTs, P) =
-      variants_abs (aTs, #2 (Syntax.variant_abs(a,T,P)));
+      variants_abs (aTs, #2 (Syntax_Trans.variant_abs(a,T,P)));
 
 (*Select subgoal i from proof state; substitute parameters, for printing*)
 fun prepare_goal i st =
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Big_Operators.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -86,10 +86,10 @@
         if x <> y then raise Match
         else
           let
-            val x' = Syntax.mark_bound x;
+            val x' = Syntax_Trans.mark_bound x;
             val t' = subst_bound (x', t);
             val P' = subst_bound (x', P);
-          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end
+          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end
     | setsum_tr' _ = raise Match;
 in [(@{const_syntax setsum}, setsum_tr')] end
 *}
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -159,8 +159,8 @@
   "SUP x:A. B"   == "CONST SUPR A (%x. B)"
 
 print_translation {*
-  [Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
-    Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
+  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
+    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
 *} -- {* to avoid eta-contraction of body *}
 
 context complete_lattice
@@ -409,7 +409,7 @@
   "INT x:A. B"  == "CONST INTER A (%x. B)"
 
 print_translation {*
-  [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
+  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
 *} -- {* to avoid eta-contraction of body *}
 
 lemma INTER_eq_Inter_image:
@@ -612,7 +612,7 @@
 *}
 
 print_translation {*
-  [Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
+  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
 *} -- {* to avoid eta-contraction of body *}
 
 lemma UNION_eq_Union_image:
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -1924,12 +1924,12 @@
       @{code NOT} (fm_of_term ps vs t')
   | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
       let
-        val (xn', p') = variant_abs (xn, xT, p);
+        val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
       in @{code E} (fm_of_term ps vs' p) end
   | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
       let
-        val (xn', p') = variant_abs (xn, xT, p);
+        val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
       in @{code A} (fm_of_term ps vs' p) end
   | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
@@ -1988,7 +1988,7 @@
         else insert (op aconv) t acc
     | f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a  
         else insert (op aconv) t acc
-    | Abs p => term_bools acc (snd (variant_abs p))
+    | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
     | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
   end;
 
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -2939,13 +2939,13 @@
   | Const(@{const_name Orderings.less_eq},_)$p$q => 
         @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
   | Const(@{const_name Ex},_)$Abs(xn,xT,p) => 
-     let val (xn', p') =  variant_abs (xn,xT,p)
+     let val (xn', p') = Syntax_Trans.variant_abs (xn,xT,p)  (* FIXME !? *)
          val x = Free(xn',xT)
          fun incr i = i + 1
          val m0 = (x,0):: (map (apsnd incr) m)
       in @{code E} (fm_of_term m0 m' p') end
   | Const(@{const_name All},_)$Abs(xn,xT,p) => 
-     let val (xn', p') =  variant_abs (xn,xT,p)
+     let val (xn', p') = Syntax_Trans.variant_abs (xn,xT,p)  (* FIXME !? *)
          val x = Free(xn',xT)
          fun incr i = i + 1
          val m0 = (x,0):: (map (apsnd incr) m)
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -130,7 +130,7 @@
 
 print_translation {*
   [(@{const_syntax The}, fn [Abs abs] =>
-      let val (x, t) = atomic_abs_tr' abs
+      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
       in Syntax.const @{syntax_const "_The"} $ x $ t end)]
 *}  -- {* To avoid eta-contraction of body *}
 
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -34,12 +34,12 @@
 
 parse_translation {*
 (* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
-  [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
+  [Syntax_Trans.mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
 *}
 
 print_translation {*
   [(@{const_syntax Abs_cfun}, fn [Abs abs] =>
-      let val (x, t) = atomic_abs_tr' abs
+      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
       in Syntax.const @{syntax_const "_cabs"} $ x $ t end)]
 *}  -- {* To avoid eta-contraction of body *}
 
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -132,7 +132,7 @@
 (* rewrite (_pat x) => (succeed) *)
 (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
  [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
-  mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
+  Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
 *}
 
 text {* Printing Case expressions *}
@@ -154,7 +154,7 @@
             val abs =
               case t of Abs abs => abs
                 | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
-            val (x, t') = atomic_abs_tr' abs;
+            val (x, t') = Syntax_Trans.atomic_abs_tr' abs;
           in (Syntax.const @{syntax_const "_variable"} $ x, t') end
     |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
 
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -26,7 +26,7 @@
 
 print_translation {*
   [(@{const_syntax Eps}, fn [Abs abs] =>
-      let val (x, t) = atomic_abs_tr' abs
+      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
       in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
 *} -- {* to avoid eta-contraction of body *}
 
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Hoare/hoare_syntax.ML
--- a/src/HOL/Hoare/hoare_syntax.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Hoare/hoare_syntax.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -26,9 +26,9 @@
     (SOME x, SOME y) => x = y
   | _ => false);
 
-fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
+fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
   | mk_abstuple (x :: xs) body =
-      Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
+      Syntax.const @{const_syntax prod_case} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
 
 fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
   | mk_fbody x e (y :: xs) =
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Hoare_Parallel/OG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -76,11 +76,11 @@
 print_translation {*
   let
     fun quote_tr' f (t :: ts) =
-          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
+          Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
       | quote_tr' _ _ = raise Match;
 
     fun annquote_tr' f (r :: t :: ts) =
-          Term.list_comb (f $ r $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
+          Term.list_comb (f $ r $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
       | annquote_tr' _ _ = raise Match;
 
     val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
@@ -94,13 +94,13 @@
       | annbexp_tr' _ _ = raise Match;
 
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
-          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
+          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
+            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
 
     fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
-          quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
+          quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f)
+            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
       | annassign_tr' _ = raise Match;
 
     fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Hoare_Parallel/Quote_Antiquote.thy
--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -16,7 +16,7 @@
 
 parse_translation {*
   let
-    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
+    fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
       | quote_tr ts = raise TERM ("quote_tr", ts);
   in [(@{syntax_const "_quote"}, quote_tr)] end
 *}
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Hoare_Parallel/RG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -58,7 +58,7 @@
 print_translation {*
   let
     fun quote_tr' f (t :: ts) =
-          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
+          Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
       | quote_tr' _ _ = raise Match;
 
     val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
@@ -68,8 +68,8 @@
       | bexp_tr' _ _ = raise Match;
 
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
-          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
+          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
+            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in
    [(@{const_syntax Collect}, assert_tr'),
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -185,8 +185,8 @@
   of the concrete syntactic representation of our Hoare language, the
   actual ``ML drivers'' is quite involved.  Just note that the we
   re-use the basic quote/antiquote translations as already defined in
-  Isabelle/Pure (see \verb,Syntax.quote_tr, and
-  \verb,Syntax.quote_tr',). *}
+  Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and
+  @{ML Syntax_Trans.quote_tr'},). *}
 
 syntax
   "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)" [0] 1000)
@@ -215,7 +215,7 @@
 
 parse_translation {*
   let
-    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
+    fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
       | quote_tr ts = raise TERM ("quote_tr", ts);
   in [(@{syntax_const "_quote"}, quote_tr)] end
 *}
@@ -228,7 +228,7 @@
 print_translation {*
   let
     fun quote_tr' f (t :: ts) =
-          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
+          Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
       | quote_tr' _ _ = raise Match;
 
     val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
@@ -238,8 +238,8 @@
       | bexp_tr' _ _ = raise Match;
 
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
-          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
+          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
+            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in
    [(@{const_syntax Collect}, assert_tr'),
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Library/reflection.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -125,7 +125,7 @@
              Abs(xn,xT,ta) => (
                let
                  val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt
-                 val (xn,ta) = variant_abs (xn,xT,ta)
+                 val (xn,ta) = Syntax_Trans.variant_abs (xn,xT,ta)  (* FIXME !? *)
                  val x = Free(xn,xT)
                  val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT)
                           of NONE => error "tryabsdecomp: Type not found in the Environement"
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Orderings.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -660,7 +660,7 @@
       Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v'
     | _ => false);
   fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
-  fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P;
+  fun mk v c n P = Syntax.const c $ Syntax_Trans.mark_bound v $ n $ P;
 
   fun tr' q = (q,
     fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _),
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Product_Type.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -199,8 +199,8 @@
   fun split_tr' [Abs (x, T, t as (Abs abs))] =
         (* split (%x y. t) => %(x,y) t *)
         let
-          val (y, t') = atomic_abs_tr' abs;
-          val (x', t'') = atomic_abs_tr' (x, T, t');
+          val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
+          val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
         in
           Syntax.const @{syntax_const "_abs"} $
             (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
@@ -210,7 +210,7 @@
         let
           val Const (@{syntax_const "_abs"}, _) $
             (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
-          val (x', t'') = atomic_abs_tr' (x, T, t');
+          val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
         in
           Syntax.const @{syntax_const "_abs"} $
             (Syntax.const @{syntax_const "_pattern"} $ x' $
@@ -221,7 +221,7 @@
         split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
     | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
         (* split (%pttrn z. t) => %(pttrn,z). t *)
-        let val (z, t) = atomic_abs_tr' abs in
+        let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
           Syntax.const @{syntax_const "_abs"} $
             (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
         end
@@ -239,8 +239,8 @@
         | _ =>
           let 
             val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
-            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
-            val (x', t'') = atomic_abs_tr' (x, xT, t');
+            val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
+            val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
           in
             Syntax.const @{syntax_const "_abs"} $
               (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
@@ -251,8 +251,9 @@
         | _ =>
           let
             val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
-            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
-            val (x', t'') = atomic_abs_tr' ("x", xT, t');
+            val (y, t') =
+              Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
+            val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
           in
             Syntax.const @{syntax_const "_abs"} $
               (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
@@ -276,10 +277,10 @@
     | _ => f ts;
   fun contract2 (Q,f) = (Q, contract Q f);
   val pairs =
-    [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
-     Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
-     Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
-     Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
+    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
+     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
+     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
+     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
 in map contract2 pairs end
 *}
 
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Set.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -246,7 +246,7 @@
 
   fun mk v v' c n P =
     if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
-    then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match;
+    then Syntax.const c $ Syntax_Trans.mark_bound v' $ n $ P else raise Match;
 
   fun tr' q = (q,
         fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (T, _)),
@@ -275,7 +275,7 @@
 
 parse_translation {*
   let
-    val ex_tr = snd (mk_binder_tr ("EX ", @{const_syntax Ex}));
+    val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", @{const_syntax Ex}));
 
     fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1
       | nvars _ = 1;
@@ -291,13 +291,13 @@
 *}
 
 print_translation {*
- [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
-  Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
+ [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
+  Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
 *} -- {* to avoid eta-contraction of body *}
 
 print_translation {*
 let
-  val ex_tr' = snd (mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
+  val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
 
   fun setcompr_tr' [Abs (abs as (_, _, P))] =
     let
@@ -315,7 +315,7 @@
       if check (P, 0) then tr' P
       else
         let
-          val (x as _ $ Free(xN, _), t) = atomic_abs_tr' abs;
+          val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs;
           val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
         in
           case t of
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -454,12 +454,12 @@
       let val xs = Term.add_frees pat [] in
         Syntax.const @{syntax_const "_case1"} $
           map_aterms
-            (fn Free p => Syntax.mark_boundT p
+            (fn Free p => Syntax_Trans.mark_boundT p
               | Const (s, _) => Syntax.const (Syntax.mark_const s)
               | t => t) pat $
           map_aterms
             (fn x as Free (s, T) =>
-                  if member (op =) xs (s, T) then Syntax.mark_bound s else x
+                  if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
               | t => t) rhs
       end;
   in
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -579,13 +579,13 @@
               else insert (op aconv) t
     | f $ a => if skip orelse is_op f then add_bools a o add_bools f
               else insert (op aconv) t
-    | Abs p => add_bools (snd (variant_abs p))
+    | Abs p => add_bools (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
     | _ => if skip orelse is_op t then I else insert (op aconv) t
   end;
 
 fun descend vs (abs as (_, xT, _)) =
   let
-    val (xn', p') = variant_abs abs;
+    val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
   in ((xn', xT) :: vs, p') end;
 
 local structure Proc = Cooper_Procedure in
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Tools/record.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -963,7 +963,7 @@
 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
       (case dest_update ctxt c of
         SOME name =>
-          (case try Syntax.const_abs_tr' k of
+          (case try Syntax_Trans.const_abs_tr' k of
             SOME t =>
               apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
                 (field_updates_tr' ctxt u)
diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/ex/Antiquote.thy
--- a/src/HOL/ex/Antiquote.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/ex/Antiquote.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -25,11 +25,13 @@
   where "Expr exp env = exp env"
 
 parse_translation {*
-  [Syntax.quote_antiquote_tr @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
+  [Syntax_Trans.quote_antiquote_tr
+    @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
 *}
 
 print_translation {*
-  [Syntax.quote_antiquote_tr' @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
+  [Syntax_Trans.quote_antiquote_tr'
+    @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
 *}
 
 term "EXPR (a + b + c)"
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/IsaMakefile	Fri Apr 08 13:31:16 2011 +0200
@@ -185,9 +185,9 @@
   Syntax/printer.ML					\
   Syntax/simple_syntax.ML				\
   Syntax/syn_ext.ML					\
-  Syntax/syn_trans.ML					\
   Syntax/syntax.ML					\
   Syntax/syntax_phases.ML				\
+  Syntax/syntax_trans.ML				\
   Syntax/term_position.ML				\
   System/isabelle_process.ML				\
   System/isabelle_system.ML				\
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -407,7 +407,7 @@
   register_config Syntax.show_structs_raw #>
   register_config Syntax.show_question_marks_raw #>
   register_config Syntax.ambiguity_level_raw #>
-  register_config Syntax.eta_contract_raw #>
+  register_config Syntax_Trans.eta_contract_raw #>
   register_config ML_Context.trace_raw #>
   register_config ProofContext.show_abbrevs_raw #>
   register_config Goal_Display.goals_limit_raw #>
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Isar/obtain.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -231,7 +231,7 @@
       handle Type.TUNIFY =>
         err ("Failed to unify variable " ^
           string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^
-          string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
+          string_of_term (Syntax_Trans.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
     val (tyenv, _) = fold unify (map #1 vars ~~ take m params)
       (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
     val norm_type = Envir.norm_type tyenv;
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -133,7 +133,7 @@
   bool_pref Goal_Display.show_main_goal_default
     "show-main-goal"
     "Show main goal in proof state display",
-  bool_pref Syntax.eta_contract_default
+  bool_pref Syntax_Trans.eta_contract_default
     "eta-contract"
     "Print terms eta-contracted"];
 
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/ROOT.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -124,7 +124,7 @@
 use "Syntax/ast.ML";
 use "Syntax/syn_ext.ML";
 use "Syntax/parser.ML";
-use "Syntax/syn_trans.ML";
+use "Syntax/syntax_trans.ML";
 use "Syntax/mixfix.ML";
 use "Syntax/printer.ML";
 use "Syntax/syntax.ML";
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -58,7 +58,7 @@
       | update_gram ((false, add, m), decls) =
           Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
 
-    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
+    val (atrs, trs, trs', atrs') = Syntax_Trans.struct_trfuns structs;
     val local_syntax = thy_syntax
       |> Syntax.update_trfuns
           (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -154,10 +154,10 @@
     val xconsts = map #1 const_decls;
     val binders = map_filter binder const_decls;
     val binder_trs = binders
-      |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syn_Trans.mk_binder_tr);
+      |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
     val binder_trs' = binders
       |> map (Syn_Ext.stamp_trfun binder_stamp o
-          apsnd (K o Syn_Trans.non_typed_tr') o Syn_Trans.mk_binder_tr' o swap);
+          apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
   in
     Syn_Ext.syn_ext' true is_logtype
       mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -173,9 +173,9 @@
 
     (*default applications: prefix / postfix*)
     val appT =
-      if type_mode then Syn_Trans.tappl_ast_tr'
-      else if curried then Syn_Trans.applC_ast_tr'
-      else Syn_Trans.appl_ast_tr';
+      if type_mode then Syntax_Trans.tappl_ast_tr'
+      else if curried then Syntax_Trans.applC_ast_tr'
+      else Syntax_Trans.appl_ast_tr';
 
     fun synT _ ([], args) = ([], args)
       | synT m (Arg p :: symbs, t :: args) =
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Fri Apr 08 11:39:45 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,560 +0,0 @@
-(*  Title:      Pure/Syntax/syn_trans.ML
-    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
-
-Syntax translation functions.
-*)
-
-signature SYN_TRANS0 =
-sig
-  val eta_contract_default: bool Unsynchronized.ref
-  val eta_contract_raw: Config.raw
-  val eta_contract: bool Config.T
-  val atomic_abs_tr': string * typ * term -> term * term
-  val const_abs_tr': term -> term
-  val mk_binder_tr: string * string -> string * (term list -> term)
-  val mk_binder_tr': string * string -> string * (term list -> term)
-  val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
-  val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
-  val dependent_tr': string * string -> term list -> term
-  val antiquote_tr: string -> term -> term
-  val quote_tr: string -> term -> term
-  val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)
-  val antiquote_tr': string -> term -> term
-  val quote_tr': string -> term -> term
-  val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
-  val update_name_tr': term -> term
-  val mark_bound: string -> term
-  val mark_boundT: string * typ -> term
-  val bound_vars: (string * typ) list -> term -> term
-  val variant_abs: string * typ * term -> string * term
-  val variant_abs': string * typ * term -> string * term
-end;
-
-signature SYN_TRANS1 =
-sig
-  include SYN_TRANS0
-  val no_brackets: unit -> bool
-  val no_type_brackets: unit -> bool
-  val non_typed_tr': (term list -> term) -> typ -> term list -> term
-  val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
-  val constrainAbsC: string
-  val abs_tr: term list -> term
-  val pure_trfuns:
-    (string * (Ast.ast list -> Ast.ast)) list *
-    (string * (term list -> term)) list *
-    (string * (term list -> term)) list *
-    (string * (Ast.ast list -> Ast.ast)) list
-  val struct_trfuns: string list ->
-    (string * (Ast.ast list -> Ast.ast)) list *
-    (string * (term list -> term)) list *
-    (string * (typ -> term list -> term)) list *
-    (string * (Ast.ast list -> Ast.ast)) list
-end;
-
-signature SYN_TRANS =
-sig
-  include SYN_TRANS1
-  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
-  val abs_tr': Proof.context -> term -> term
-  val prop_tr': term -> term
-  val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
-  val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
-end;
-
-structure Syn_Trans: SYN_TRANS =
-struct
-
-(* print mode *)
-
-val bracketsN = "brackets";
-val no_bracketsN = "no_brackets";
-
-fun no_brackets () =
-  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
-    (print_mode_value ()) = SOME no_bracketsN;
-
-val type_bracketsN = "type_brackets";
-val no_type_bracketsN = "no_type_brackets";
-
-fun no_type_brackets () =
-  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
-    (print_mode_value ()) <> SOME type_bracketsN;
-
-
-
-(** parse (ast) translations **)
-
-(* strip_positions *)
-
-fun strip_positions_ast_tr [ast] = Ast.strip_positions ast
-  | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
-
-
-(* constify *)
-
-fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
-  | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
-
-
-(* type syntax *)
-
-fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
-  | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
-
-fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
-  | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
-
-fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
-  | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
-
-
-(* application *)
-
-fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)
-  | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);
-
-fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args)
-  | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts);
-
-
-(* abstraction *)
-
-fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
-  | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
-
-fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]
-  | idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
-
-fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
-  | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
-
-val constrainAbsC = "_constrainAbs";
-
-fun absfree_proper (x, T, t) =
-  if can Name.dest_internal x
-  then error ("Illegal internal variable in abstraction: " ^ quote x)
-  else Term.absfree (x, T, t);
-
-fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
-  | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
-  | abs_tr [Const ("_constrain", _) $ x $ tT, t] = Lexicon.const constrainAbsC $ abs_tr [x, t] $ tT
-  | abs_tr ts = raise TERM ("abs_tr", ts);
-
-
-(* binder *)
-
-fun mk_binder_tr (syn, name) =
-  let
-    fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
-    fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
-      | binder_tr [x, t] =
-          let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
-          in Lexicon.const name $ abs end
-      | binder_tr ts = err ts;
-  in (syn, binder_tr) end;
-
-
-(* type propositions *)
-
-fun mk_type ty =
-  Lexicon.const "_constrain" $
-    Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
-
-fun ofclass_tr [ty, cls] = cls $ mk_type ty
-  | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
-
-fun sort_constraint_tr [ty] = Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty
-  | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
-
-
-(* meta propositions *)
-
-fun aprop_tr [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
-  | aprop_tr ts = raise TERM ("aprop_tr", ts);
-
-
-(* meta implication *)
-
-fun bigimpl_ast_tr (asts as [asms, concl]) =
-      let val prems =
-        (case Ast.unfold_ast_p "_asms" asms of
-          (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
-        | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
-      in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
-  | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
-
-
-(* type/term reflection *)
-
-fun type_tr [ty] = mk_type ty
-  | type_tr ts = raise TERM ("type_tr", ts);
-
-
-(* dddot *)
-
-fun dddot_tr ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts);
-
-
-(* quote / antiquote *)
-
-fun antiquote_tr name =
-  let
-    fun tr i ((t as Const (c, _)) $ u) =
-          if c = name then tr i u $ Bound i
-          else tr i t $ tr i u
-      | tr i (t $ u) = tr i t $ tr i u
-      | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)
-      | tr _ a = a;
-  in tr 0 end;
-
-fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t));
-
-fun quote_antiquote_tr quoteN antiquoteN name =
-  let
-    fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t
-      | tr ts = raise TERM ("quote_tr", ts);
-  in (quoteN, tr) end;
-
-
-(* corresponding updates *)
-
-fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
-  | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
-  | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
-      if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
-      else
-        list_comb (c $ update_name_tr [t] $
-          (Lexicon.fun_type $
-            (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
-  | update_name_tr ts = raise TERM ("update_name_tr", ts);
-
-
-(* indexed syntax *)
-
-fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast
-  | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
-
-fun index_ast_tr ast =
-  Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];
-
-fun indexdefault_ast_tr [] = index_ast_tr (Ast.Constant "_indexdefault")
-  | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
-
-fun indexnum_ast_tr [ast] = index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])
-  | indexnum_ast_tr asts = raise Ast.AST ("indexnum_ast_tr", asts);
-
-fun indexvar_ast_tr [] = Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]
-  | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
-
-fun index_tr [t] = t
-  | index_tr ts = raise TERM ("index_tr", ts);
-
-
-(* implicit structures *)
-
-fun the_struct structs i =
-  if 1 <= i andalso i <= length structs then nth structs (i - 1)
-  else error ("Illegal reference to implicit structure #" ^ string_of_int i);
-
-fun struct_tr structs [Const ("_indexdefault", _)] =
-      Lexicon.free (the_struct structs 1)
-  | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
-      Lexicon.free (the_struct structs
-        (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
-  | struct_tr _ ts = raise TERM ("struct_tr", ts);
-
-
-
-(** print (ast) translations **)
-
-(* types *)
-
-fun non_typed_tr' f _ ts = f ts;
-fun non_typed_tr'' f x _ ts = f x ts;
-
-
-(* type syntax *)
-
-fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
-  | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
-  | tappl_ast_tr' (f, ty :: tys) =
-      Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
-
-fun fun_ast_tr' asts =
-  if no_brackets () orelse no_type_brackets () then raise Match
-  else
-    (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
-      (dom as _ :: _ :: _, cod)
-        => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
-    | _ => raise Match);
-
-
-(* application *)
-
-fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])
-  | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args];
-
-fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f])
-  | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
-
-
-(* partial eta-contraction before printing *)
-
-fun eta_abs (Abs (a, T, t)) =
-      (case eta_abs t of
-        t' as Const ("_aprop", _) $ _ => Abs (a, T, t')
-      | t' as f $ u =>
-          (case eta_abs u of
-            Bound 0 =>
-              if Term.is_dependent f then Abs (a, T, t')
-              else incr_boundvars ~1 f
-          | _ => Abs (a, T, t'))
-      | t' => Abs (a, T, t'))
-  | eta_abs t = t;
-
-val eta_contract_default = Unsynchronized.ref true;
-val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
-val eta_contract = Config.bool eta_contract_raw;
-
-fun eta_contr ctxt tm =
-  if Config.get ctxt eta_contract then eta_abs tm else tm;
-
-
-(* abstraction *)
-
-fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
-fun mark_bound x = mark_boundT (x, dummyT);
-
-fun bound_vars vars body =
-  subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);
-
-fun strip_abss vars_of body_of tm =
-  let
-    val vars = vars_of tm;
-    val body = body_of tm;
-    val rev_new_vars = Term.rename_wrt_term body vars;
-    fun subst (x, T) b =
-      if can Name.dest_internal x andalso not (Term.is_dependent b)
-      then (Const ("_idtdummy", T), incr_boundvars ~1 b)
-      else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
-    val (rev_vars', body') = fold_map subst rev_new_vars body;
-  in (rev rev_vars', body') end;
-
-
-fun abs_tr' ctxt tm =
-  uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
-    (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
-
-fun atomic_abs_tr' (x, T, t) =
-  let val [xT] = Term.rename_wrt_term t [(x, T)]
-  in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
-
-fun abs_ast_tr' asts =
-  (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
-    ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
-  | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
-
-fun const_abs_tr' t =
-  (case eta_abs t of
-    Abs (_, _, t') =>
-      if Term.is_dependent t' then raise Match
-      else incr_boundvars ~1 t'
-  | _ => raise Match);
-
-
-(* binders *)
-
-fun mk_binder_tr' (name, syn) =
-  let
-    fun mk_idts [] = raise Match    (*abort translation*)
-      | mk_idts [idt] = idt
-      | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts;
-
-    fun tr' t =
-      let
-        val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
-      in Lexicon.const syn $ mk_idts xs $ bd end;
-
-    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
-      | binder_tr' [] = raise Match;
-  in (name, binder_tr') end;
-
-fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
-  let val (x, t) = atomic_abs_tr' abs
-  in list_comb (Lexicon.const syn $ x $ t, ts) end);
-
-fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
-  let val (x, t) = atomic_abs_tr' abs
-  in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
-
-
-(* idtyp constraints *)
-
-fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
-      Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
-  | idtyp_ast_tr' _ _ = raise Match;
-
-
-(* meta propositions *)
-
-fun prop_tr' tm =
-  let
-    fun aprop t = Lexicon.const "_aprop" $ t;
-
-    fun is_prop Ts t =
-      fastype_of1 (Ts, t) = propT handle TERM _ => false;
-
-    fun is_term (Const ("Pure.term", _) $ _) = true
-      | is_term _ = false;
-
-    fun tr' _ (t as Const _) = t
-      | tr' Ts (t as Const ("_bound", _) $ u) =
-          if is_prop Ts u then aprop t else t
-      | tr' _ (t as Free (x, T)) =
-          if T = propT then aprop (Lexicon.free x) else t
-      | tr' _ (t as Var (xi, T)) =
-          if T = propT then aprop (Lexicon.var xi) else t
-      | tr' Ts (t as Bound _) =
-          if is_prop Ts t then aprop t else t
-      | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
-      | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
-          if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
-          else tr' Ts t1 $ tr' Ts t2
-      | tr' Ts (t as t1 $ t2) =
-          (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
-            then I else aprop) (tr' Ts t1 $ tr' Ts t2);
-  in tr' [] tm end;
-
-
-(* meta implication *)
-
-fun impl_ast_tr' asts =
-  if no_brackets () then raise Match
-  else
-    (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
-      (prems as _ :: _ :: _, concl) =>
-        let
-          val (asms, asm) = split_last prems;
-          val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);
-        in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end
-    | _ => raise Match);
-
-
-(* dependent / nondependent quantifiers *)
-
-fun var_abs mark (x, T, b) =
-  let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
-  in (x', subst_bound (mark (x', T), b)) end;
-
-val variant_abs = var_abs Free;
-val variant_abs' = var_abs mark_boundT;
-
-fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
-      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 $ incr_boundvars ~1 B, ts)
-  | dependent_tr' _ _ = raise Match;
-
-
-(* quote / antiquote *)
-
-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
-      | 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;
-
-fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)
-  | quote_tr' _ _ = raise Match;
-
-fun quote_antiquote_tr' quoteN antiquoteN name =
-  let
-    fun tr' (t :: ts) = Term.list_comb (Lexicon.const quoteN $ quote_tr' antiquoteN t, ts)
-      | tr' _ = raise Match;
-  in (name, tr') end;
-
-
-(* corresponding updates *)
-
-local
-
-fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
-  | upd_type _ = dummyT;
-
-fun upd_tr' (x_upd, T) =
-  (case try (unsuffix "_update") x_upd of
-    SOME x => (x, upd_type T)
-  | NONE => raise Match);
-
-in
-
-fun update_name_tr' (Free x) = Free (upd_tr' x)
-  | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
-  | update_name_tr' (Const x) = Const (upd_tr' x)
-  | update_name_tr' _ = raise Match;
-
-end;
-
-
-(* indexed syntax *)
-
-fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
-  | index_ast_tr' _ = raise Match;
-
-
-(* implicit structures *)
-
-fun the_struct' structs s =
-  [(case Lexicon.read_nat s of
-    SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)
-  | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
-
-fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = the_struct' structs "1"
-  | struct_ast_tr' structs [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =
-      the_struct' structs s
-  | struct_ast_tr' _ _ = raise Match;
-
-
-
-(** Pure translations **)
-
-val pure_trfuns =
-  ([("_strip_positions", strip_positions_ast_tr),
-    ("_constify", constify_ast_tr),
-    ("_tapp", tapp_ast_tr),
-    ("_tappl", tappl_ast_tr),
-    ("_bracket", bracket_ast_tr),
-    ("_appl", appl_ast_tr),
-    ("_applC", applC_ast_tr),
-    ("_lambda", lambda_ast_tr),
-    ("_idtyp", idtyp_ast_tr),
-    ("_idtypdummy", idtypdummy_ast_tr),
-    ("_bigimpl", bigimpl_ast_tr),
-    ("_indexdefault", indexdefault_ast_tr),
-    ("_indexnum", indexnum_ast_tr),
-    ("_indexvar", indexvar_ast_tr),
-    ("_struct", struct_ast_tr)],
-   [("_abs", abs_tr),
-    ("_aprop", aprop_tr),
-    ("_ofclass", ofclass_tr),
-    ("_sort_constraint", sort_constraint_tr),
-    ("_TYPE", type_tr),
-    ("_DDDOT", dddot_tr),
-    ("_update_name", update_name_tr),
-    ("_index", index_tr)],
-   ([]: (string * (term list -> term)) list),
-   [("\\<^type>fun", fun_ast_tr'),
-    ("_abs", abs_ast_tr'),
-    ("_idts", idtyp_ast_tr' "_idts"),
-    ("_pttrns", idtyp_ast_tr' "_pttrns"),
-    ("\\<^const>==>", impl_ast_tr'),
-    ("_index", index_ast_tr')]);
-
-fun struct_trfuns structs =
-  ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
-
-end;
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -7,7 +7,6 @@
 
 signature BASIC_SYNTAX =
 sig
-  include SYN_TRANS0
   include MIXFIX0
   include PRINTER0
 end;
@@ -16,7 +15,6 @@
 sig
   include LEXICON0
   include SYN_EXT0
-  include SYN_TRANS1
   include MIXFIX1
   include PRINTER0
   val positions_raw: Config.raw
@@ -727,7 +725,7 @@
 
 (*export parts of internal Syntax structures*)
 val syntax_tokenize = tokenize;
-open Lexicon Syn_Ext Syn_Trans Mixfix Printer;
+open Lexicon Syn_Ext Mixfix Printer;
 val tokenize = syntax_tokenize;
 
 end;
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -532,7 +532,7 @@
 
     fun ast_of tm =
       (case strip_comb tm of
-        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
+        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
       | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
       | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
@@ -557,7 +557,7 @@
       else simple_ast_of ctxt t;
   in
     tm
-    |> Syn_Trans.prop_tr'
+    |> Syntax_Trans.prop_tr'
     |> show_types ? (#1 o prune_typs o rpair [])
     |> mark_atoms
     |> ast_of
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/Syntax/syntax_trans.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/syntax_trans.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -0,0 +1,556 @@
+(*  Title:      Pure/Syntax/syntax_trans.ML
+    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
+
+Syntax translation functions.
+*)
+
+signature BASIC_SYNTAX_TRANS =
+sig
+  val eta_contract: bool Config.T
+end
+
+signature SYNTAX_TRANS =
+sig
+  include BASIC_SYNTAX_TRANS
+  val no_brackets: unit -> bool
+  val no_type_brackets: unit -> bool
+  val abs_tr: term list -> term
+  val mk_binder_tr: string * string -> string * (term list -> term)
+  val antiquote_tr: string -> term -> term
+  val quote_tr: string -> term -> term
+  val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)
+  val non_typed_tr': (term list -> term) -> typ -> term list -> term
+  val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
+  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
+  val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
+  val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
+  val eta_contract_default: bool Unsynchronized.ref
+  val eta_contract_raw: Config.raw
+  val mark_bound: string -> term
+  val mark_boundT: string * typ -> term
+  val bound_vars: (string * typ) list -> term -> term
+  val abs_tr': Proof.context -> term -> term
+  val atomic_abs_tr': string * typ * term -> term * term
+  val const_abs_tr': term -> term
+  val mk_binder_tr': string * string -> string * (term list -> term)
+  val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
+  val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
+  val prop_tr': term -> term
+  val variant_abs: string * typ * term -> string * term
+  val variant_abs': string * typ * term -> string * term
+  val dependent_tr': string * string -> term list -> term
+  val antiquote_tr': string -> term -> term
+  val quote_tr': string -> term -> term
+  val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
+  val update_name_tr': term -> term
+  val pure_trfuns:
+    (string * (Ast.ast list -> Ast.ast)) list *
+    (string * (term list -> term)) list *
+    (string * (term list -> term)) list *
+    (string * (Ast.ast list -> Ast.ast)) list
+  val struct_trfuns: string list ->
+    (string * (Ast.ast list -> Ast.ast)) list *
+    (string * (term list -> term)) list *
+    (string * (typ -> term list -> term)) list *
+    (string * (Ast.ast list -> Ast.ast)) list
+end;
+
+structure Syntax_Trans: SYNTAX_TRANS =
+struct
+
+(* print mode *)
+
+val bracketsN = "brackets";
+val no_bracketsN = "no_brackets";
+
+fun no_brackets () =
+  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
+    (print_mode_value ()) = SOME no_bracketsN;
+
+val type_bracketsN = "type_brackets";
+val no_type_bracketsN = "no_type_brackets";
+
+fun no_type_brackets () =
+  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
+    (print_mode_value ()) <> SOME type_bracketsN;
+
+
+
+(** parse (ast) translations **)
+
+(* strip_positions *)
+
+fun strip_positions_ast_tr [ast] = Ast.strip_positions ast
+  | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
+
+
+(* constify *)
+
+fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
+  | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
+
+
+(* type syntax *)
+
+fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
+  | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
+
+fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
+  | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
+
+fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
+  | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
+
+
+(* application *)
+
+fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)
+  | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);
+
+fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args)
+  | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts);
+
+
+(* abstraction *)
+
+fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
+  | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
+
+fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]
+  | idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
+
+fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
+  | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
+
+fun absfree_proper (x, T, t) =
+  if can Name.dest_internal x
+  then error ("Illegal internal variable in abstraction: " ^ quote x)
+  else Term.absfree (x, T, t);
+
+fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
+  | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
+  | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
+      Lexicon.const "_constrainAbs" $ abs_tr [x, t] $ tT
+  | abs_tr ts = raise TERM ("abs_tr", ts);
+
+
+(* binder *)
+
+fun mk_binder_tr (syn, name) =
+  let
+    fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
+    fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
+      | binder_tr [x, t] =
+          let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
+          in Lexicon.const name $ abs end
+      | binder_tr ts = err ts;
+  in (syn, binder_tr) end;
+
+
+(* type propositions *)
+
+fun mk_type ty =
+  Lexicon.const "_constrain" $
+    Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
+
+fun ofclass_tr [ty, cls] = cls $ mk_type ty
+  | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
+
+fun sort_constraint_tr [ty] = Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty
+  | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
+
+
+(* meta propositions *)
+
+fun aprop_tr [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
+  | aprop_tr ts = raise TERM ("aprop_tr", ts);
+
+
+(* meta implication *)
+
+fun bigimpl_ast_tr (asts as [asms, concl]) =
+      let val prems =
+        (case Ast.unfold_ast_p "_asms" asms of
+          (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
+        | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
+      in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
+  | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
+
+
+(* type/term reflection *)
+
+fun type_tr [ty] = mk_type ty
+  | type_tr ts = raise TERM ("type_tr", ts);
+
+
+(* dddot *)
+
+fun dddot_tr ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts);
+
+
+(* quote / antiquote *)
+
+fun antiquote_tr name =
+  let
+    fun tr i ((t as Const (c, _)) $ u) =
+          if c = name then tr i u $ Bound i
+          else tr i t $ tr i u
+      | tr i (t $ u) = tr i t $ tr i u
+      | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)
+      | tr _ a = a;
+  in tr 0 end;
+
+fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t));
+
+fun quote_antiquote_tr quoteN antiquoteN name =
+  let
+    fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t
+      | tr ts = raise TERM ("quote_tr", ts);
+  in (quoteN, tr) end;
+
+
+(* corresponding updates *)
+
+fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
+  | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
+  | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
+      if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
+      else
+        list_comb (c $ update_name_tr [t] $
+          (Lexicon.fun_type $
+            (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
+  | update_name_tr ts = raise TERM ("update_name_tr", ts);
+
+
+(* indexed syntax *)
+
+fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast
+  | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
+
+fun index_ast_tr ast =
+  Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];
+
+fun indexdefault_ast_tr [] = index_ast_tr (Ast.Constant "_indexdefault")
+  | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
+
+fun indexnum_ast_tr [ast] = index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])
+  | indexnum_ast_tr asts = raise Ast.AST ("indexnum_ast_tr", asts);
+
+fun indexvar_ast_tr [] = Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]
+  | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
+
+fun index_tr [t] = t
+  | index_tr ts = raise TERM ("index_tr", ts);
+
+
+(* implicit structures *)
+
+fun the_struct structs i =
+  if 1 <= i andalso i <= length structs then nth structs (i - 1)
+  else error ("Illegal reference to implicit structure #" ^ string_of_int i);
+
+fun struct_tr structs [Const ("_indexdefault", _)] =
+      Lexicon.free (the_struct structs 1)
+  | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
+      Lexicon.free (the_struct structs
+        (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
+  | struct_tr _ ts = raise TERM ("struct_tr", ts);
+
+
+
+(** print (ast) translations **)
+
+(* types *)
+
+fun non_typed_tr' f _ ts = f ts;
+fun non_typed_tr'' f x _ ts = f x ts;
+
+
+(* type syntax *)
+
+fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
+  | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
+  | tappl_ast_tr' (f, ty :: tys) =
+      Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
+
+fun fun_ast_tr' asts =
+  if no_brackets () orelse no_type_brackets () then raise Match
+  else
+    (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
+      (dom as _ :: _ :: _, cod)
+        => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
+    | _ => raise Match);
+
+
+(* application *)
+
+fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])
+  | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args];
+
+fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f])
+  | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
+
+
+(* partial eta-contraction before printing *)
+
+fun eta_abs (Abs (a, T, t)) =
+      (case eta_abs t of
+        t' as Const ("_aprop", _) $ _ => Abs (a, T, t')
+      | t' as f $ u =>
+          (case eta_abs u of
+            Bound 0 =>
+              if Term.is_dependent f then Abs (a, T, t')
+              else incr_boundvars ~1 f
+          | _ => Abs (a, T, t'))
+      | t' => Abs (a, T, t'))
+  | eta_abs t = t;
+
+val eta_contract_default = Unsynchronized.ref true;
+val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
+val eta_contract = Config.bool eta_contract_raw;
+
+fun eta_contr ctxt tm =
+  if Config.get ctxt eta_contract then eta_abs tm else tm;
+
+
+(* abstraction *)
+
+fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
+fun mark_bound x = mark_boundT (x, dummyT);
+
+fun bound_vars vars body =
+  subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);
+
+fun strip_abss vars_of body_of tm =
+  let
+    val vars = vars_of tm;
+    val body = body_of tm;
+    val rev_new_vars = Term.rename_wrt_term body vars;
+    fun subst (x, T) b =
+      if can Name.dest_internal x andalso not (Term.is_dependent b)
+      then (Const ("_idtdummy", T), incr_boundvars ~1 b)
+      else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
+    val (rev_vars', body') = fold_map subst rev_new_vars body;
+  in (rev rev_vars', body') end;
+
+
+fun abs_tr' ctxt tm =
+  uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
+    (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
+
+fun atomic_abs_tr' (x, T, t) =
+  let val [xT] = Term.rename_wrt_term t [(x, T)]
+  in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
+
+fun abs_ast_tr' asts =
+  (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
+    ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
+  | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
+
+fun const_abs_tr' t =
+  (case eta_abs t of
+    Abs (_, _, t') =>
+      if Term.is_dependent t' then raise Match
+      else incr_boundvars ~1 t'
+  | _ => raise Match);
+
+
+(* binders *)
+
+fun mk_binder_tr' (name, syn) =
+  let
+    fun mk_idts [] = raise Match    (*abort translation*)
+      | mk_idts [idt] = idt
+      | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts;
+
+    fun tr' t =
+      let
+        val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
+      in Lexicon.const syn $ mk_idts xs $ bd end;
+
+    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
+      | binder_tr' [] = raise Match;
+  in (name, binder_tr') end;
+
+fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
+  let val (x, t) = atomic_abs_tr' abs
+  in list_comb (Lexicon.const syn $ x $ t, ts) end);
+
+fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
+  let val (x, t) = atomic_abs_tr' abs
+  in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
+
+
+(* idtyp constraints *)
+
+fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
+      Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
+  | idtyp_ast_tr' _ _ = raise Match;
+
+
+(* meta propositions *)
+
+fun prop_tr' tm =
+  let
+    fun aprop t = Lexicon.const "_aprop" $ t;
+
+    fun is_prop Ts t =
+      fastype_of1 (Ts, t) = propT handle TERM _ => false;
+
+    fun is_term (Const ("Pure.term", _) $ _) = true
+      | is_term _ = false;
+
+    fun tr' _ (t as Const _) = t
+      | tr' Ts (t as Const ("_bound", _) $ u) =
+          if is_prop Ts u then aprop t else t
+      | tr' _ (t as Free (x, T)) =
+          if T = propT then aprop (Lexicon.free x) else t
+      | tr' _ (t as Var (xi, T)) =
+          if T = propT then aprop (Lexicon.var xi) else t
+      | tr' Ts (t as Bound _) =
+          if is_prop Ts t then aprop t else t
+      | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
+      | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
+          if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
+          else tr' Ts t1 $ tr' Ts t2
+      | tr' Ts (t as t1 $ t2) =
+          (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
+            then I else aprop) (tr' Ts t1 $ tr' Ts t2);
+  in tr' [] tm end;
+
+
+(* meta implication *)
+
+fun impl_ast_tr' asts =
+  if no_brackets () then raise Match
+  else
+    (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
+      (prems as _ :: _ :: _, concl) =>
+        let
+          val (asms, asm) = split_last prems;
+          val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);
+        in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end
+    | _ => raise Match);
+
+
+(* dependent / nondependent quantifiers *)
+
+fun var_abs mark (x, T, b) =
+  let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
+  in (x', subst_bound (mark (x', T), b)) end;
+
+val variant_abs = var_abs Free;
+val variant_abs' = var_abs mark_boundT;
+
+fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
+      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 $ incr_boundvars ~1 B, ts)
+  | dependent_tr' _ _ = raise Match;
+
+
+(* quote / antiquote *)
+
+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
+      | 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;
+
+fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)
+  | quote_tr' _ _ = raise Match;
+
+fun quote_antiquote_tr' quoteN antiquoteN name =
+  let
+    fun tr' (t :: ts) = Term.list_comb (Lexicon.const quoteN $ quote_tr' antiquoteN t, ts)
+      | tr' _ = raise Match;
+  in (name, tr') end;
+
+
+(* corresponding updates *)
+
+local
+
+fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
+  | upd_type _ = dummyT;
+
+fun upd_tr' (x_upd, T) =
+  (case try (unsuffix "_update") x_upd of
+    SOME x => (x, upd_type T)
+  | NONE => raise Match);
+
+in
+
+fun update_name_tr' (Free x) = Free (upd_tr' x)
+  | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
+  | update_name_tr' (Const x) = Const (upd_tr' x)
+  | update_name_tr' _ = raise Match;
+
+end;
+
+
+(* indexed syntax *)
+
+fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
+  | index_ast_tr' _ = raise Match;
+
+
+(* implicit structures *)
+
+fun the_struct' structs s =
+  [(case Lexicon.read_nat s of
+    SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)
+  | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
+
+fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = the_struct' structs "1"
+  | struct_ast_tr' structs [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =
+      the_struct' structs s
+  | struct_ast_tr' _ _ = raise Match;
+
+
+
+(** Pure translations **)
+
+val pure_trfuns =
+  ([("_strip_positions", strip_positions_ast_tr),
+    ("_constify", constify_ast_tr),
+    ("_tapp", tapp_ast_tr),
+    ("_tappl", tappl_ast_tr),
+    ("_bracket", bracket_ast_tr),
+    ("_appl", appl_ast_tr),
+    ("_applC", applC_ast_tr),
+    ("_lambda", lambda_ast_tr),
+    ("_idtyp", idtyp_ast_tr),
+    ("_idtypdummy", idtypdummy_ast_tr),
+    ("_bigimpl", bigimpl_ast_tr),
+    ("_indexdefault", indexdefault_ast_tr),
+    ("_indexnum", indexnum_ast_tr),
+    ("_indexvar", indexvar_ast_tr),
+    ("_struct", struct_ast_tr)],
+   [("_abs", abs_tr),
+    ("_aprop", aprop_tr),
+    ("_ofclass", ofclass_tr),
+    ("_sort_constraint", sort_constraint_tr),
+    ("_TYPE", type_tr),
+    ("_DDDOT", dddot_tr),
+    ("_update_name", update_name_tr),
+    ("_index", index_tr)],
+   ([]: (string * (term list -> term)) list),
+   [("\\<^type>fun", fun_ast_tr'),
+    ("_abs", abs_ast_tr'),
+    ("_idts", idtyp_ast_tr' "_idts"),
+    ("_pttrns", idtyp_ast_tr' "_pttrns"),
+    ("\\<^const>==>", impl_ast_tr'),
+    ("_index", index_ast_tr')]);
+
+fun struct_trfuns structs =
+  ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
+
+end;
+
+structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;
+open Basic_Syntax_Trans;
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -453,7 +453,7 @@
 val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
 val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
 val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
-val _ = add_option "eta_contract" (Config.put eta_contract o boolean);
+val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
 val _ = add_option "display" (Config.put display o boolean);
 val _ = add_option "break" (Config.put break o boolean);
 val _ = add_option "quotes" (Config.put quotes o boolean);
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/primitive_defs.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -27,7 +27,7 @@
     val eq_body = Term.strip_all_body eq;
 
     val display_terms =
-      commas_quote o map (Syntax.string_of_term ctxt o Syntax.bound_vars eq_vars);
+      commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
     val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
 
     val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/pure_thy.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -128,7 +128,7 @@
     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     ("_update_name", typ "idt",                        NoSyn),
-    (Syntax.constrainAbsC, typ "'a",                   NoSyn),
+    ("_constrainAbs", typ "'a",                       NoSyn),
     ("_constrain_position", typ "id => id_position",   Delimfix "_"),
     ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
     ("_type_constraint_", typ "'a",                    NoSyn),
@@ -169,7 +169,7 @@
   #> Theory.add_deps "all" ("all", typ "('a => prop) => prop") []
   #> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
   #> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
-  #> Sign.add_trfuns Syntax.pure_trfuns
+  #> Sign.add_trfuns Syntax_Trans.pure_trfuns
   #> Sign.local_path
   #> Sign.add_consts_i
    [(Binding.name "term", typ "'a => prop", NoSyn),
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/raw_simplifier.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -306,7 +306,7 @@
   let
     val names = Term.declare_term_names t Name.context;
     val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
-    fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
+    fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T));
   in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
 
 fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/sign.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -477,9 +477,9 @@
 
 in
 
-val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax.non_typed_tr';
+val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax_Trans.non_typed_tr';
 val add_trfunsT = gen_add_trfunsT Syntax.update_trfuns;
-val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax.non_typed_tr'';
+val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax_Trans.non_typed_tr'';
 val add_advanced_trfunsT = gen_add_trfunsT Syntax.update_advanced_trfuns;
 
 end;
diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/type_infer.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -300,7 +300,7 @@
         val (Ts', Ts'') = chop (length Ts) Ts_bTs';
         fun prep t =
           let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
-          in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
+          in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
       in (map prep ts', Ts') end;
 
     fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
diff -r 25d9d836ed9c -r 326f57825e1a src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -688,7 +688,7 @@
       pair (IVar (SOME v))
   | translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
       let
-        val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
+        val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t);
         val v'' = if member (op =) (Term.add_free_names t' []) v'
           then SOME v' else NONE
       in
diff -r 25d9d836ed9c -r 326f57825e1a src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Tools/induct.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -580,7 +580,7 @@
   in
     if not (null params) then
       (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
-        commas_quote (map (Syntax.string_of_term ctxt o Syntax.mark_boundT) params));
+        commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_boundT) params));
       Seq.single rule)
     else
       let
diff -r 25d9d836ed9c -r 326f57825e1a src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Tools/misc_legacy.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -61,7 +61,7 @@
 fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
       strip_context_aux (params, H :: Hs, B)
   | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
-      let val (b, u) = Syntax.variant_abs (a, T, t)
+      let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
       in strip_context_aux ((b, T) :: params, Hs, u) end
   | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
 
diff -r 25d9d836ed9c -r 326f57825e1a src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Tools/subtyping.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -200,7 +200,7 @@
     val (Ts', Ts'') = chop (length Ts) Ts_bTs';
     fun prep t =
       let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
-      in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
+      in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
   in (map prep ts', Ts') end;
 
 fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);