src/Tools/Code/code_scala.ML

           print_var vars v
       | print_term tyvars is_pat some_thm vars fxy (t as _ `|=> _) =
           let
             val (vs_tys, body) = Code_Thingol.unfold_abs t;
             val (ps, vars') = fold_map (print_abs_head tyvars) vs_tys vars;
-            val vars' = intro_vars (map_filter fst vs_tys) vars;
           in
             brackets (ps @| print_term tyvars false some_thm vars' NOBR body)
           end
       | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
           (case Code_Thingol.unfold_const_app (#primitive case_expr)