src/HOL/Tools/case_translation.ML

           (dest_case2 u)
           (Syntax.const @{const_syntax case_nil}))
       end
   | case_tr _ _ _ = case_error "case_tr";
 
-val trfun_setup =
-  Sign.add_advanced_trfuns ([],
-    [(@{syntax_const "_case_syntax"}, case_tr true)],
-    [], []);
+val trfun_setup = Sign.parse_translation [(@{syntax_const "_case_syntax"}, case_tr true)];
 
 
 (* print translation *)
 
 fun case_tr' (_ :: x :: t :: ts) =

         list_comb (Syntax.const @{syntax_const "_case_syntax"} $ x $
           foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
             (mk_clauses t), ts)
       end;
 
-val trfun_setup' = Sign.add_trfuns
-  ([], [], [(@{const_syntax "case_guard"}, case_tr')], []);
+val trfun_setup' = Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')];
 
 
 (* declarations *)
 
 fun register raw_case_comb raw_constrs context =