src/Tools/Code/code_scala.ML

                    (is_none o tyco_syntax) deresolve tycos
               |> intro_tyvars vs;
             val simple = case eqs
              of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
               | _ => false;
-            val consts = fold Code_Thingol.add_constnames
-              (map (snd o fst) eqs) [];
             val vars1 = reserved
-              |> intro_base_names
-                   (is_none o const_syntax) deresolve consts
+              |> intro_base_names_for (is_none o const_syntax)
+                   deresolve (map (snd o fst) eqs);
             val params = if simple
               then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
               else aux_params vars1 (map (fst o fst) eqs);
             val vars2 = intro_vars params vars1;
             val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;