src/HOL/HOLCF/ex/Pattern_Match.thy

 
 parse_translation {*
 (* 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 *}
 
 syntax

     |   dest_LAM (Const (@{const_syntax Abs_cfun},_) $ t) =
           let
             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 *)
 
     fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
           let val (v, t) = dest_LAM r in