1.1 --- a/src/HOL/Set.thy	Fri Apr 08 11:39:45 2011 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Apr 08 13:31:16 2011 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4  
     1.5    fun mk v v' c n P =
     1.6      if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
     1.7 -    then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match;
     1.8 +    then Syntax.const c $ Syntax_Trans.mark_bound v' $ n $ P else raise Match;
     1.9  
    1.10    fun tr' q = (q,
    1.11          fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (T, _)),
    1.12 @@ -275,7 +275,7 @@
    1.13  
    1.14  parse_translation {*
    1.15    let
    1.16 -    val ex_tr = snd (mk_binder_tr ("EX ", @{const_syntax Ex}));
    1.17 +    val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", @{const_syntax Ex}));
    1.18  
    1.19      fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1
    1.20        | nvars _ = 1;
    1.21 @@ -291,13 +291,13 @@
    1.22  *}
    1.23  
    1.24  print_translation {*
    1.25 - [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
    1.26 -  Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
    1.27 + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
    1.28 +  Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
    1.29  *} -- {* to avoid eta-contraction of body *}
    1.30  
    1.31  print_translation {*
    1.32  let
    1.33 -  val ex_tr' = snd (mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
    1.34 +  val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
    1.35  
    1.36    fun setcompr_tr' [Abs (abs as (_, _, P))] =
    1.37      let
    1.38 @@ -315,7 +315,7 @@
    1.39        if check (P, 0) then tr' P
    1.40        else
    1.41          let
    1.42 -          val (x as _ $ Free(xN, _), t) = atomic_abs_tr' abs;
    1.43 +          val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs;
    1.44            val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
    1.45          in
    1.46            case t of