src/Tools/Code/code_target.ML

   let
     val module_name = "Code";
     val { env_var, make_destination, make_command } =
       (#check o the_fundamental thy) target;
     val env_param = getenv env_var;
-    fun ext_check env_param p =
+    fun ext_check p =
       let 
         val destination = make_destination p;
         val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
           module_name args naming program names_cs);
         val cmd = make_command env_param module_name;

       end;
   in if env_param = ""
     then if strict
       then error (env_var ^ " not set; cannot check code for " ^ target)
       else warning (env_var ^ " not set; skipped checking code for " ^ target)
-    else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
+    else Isabelle_System.with_tmp_dir "Code_Test" ext_check
   end;
 
 fun evaluation mounted_serializer prepared_program consts ((vs, ty), t) =
   let
     val _ = if Code_Thingol.contains_dict_var t then