src/HOL/Library/code_test.ML

 
 
 (* driver for OCaml *)
 
 val ocamlN = "OCaml"
-val ISABELLE_OCAMLC = "ISABELLE_OCAMLC"
+val ISABELLE_OPAM_ROOT = "ISABELLE_OPAM_ROOT"
 
 fun mk_driver_ocaml _ path _ value_name =
   let
     val generatedN = "generated.ml"
     val driverN = "driver.ml"

       "  print_string \"" ^ end_markerN ^ "\";;\n" ^
       "main ();;"
 
     val compiled_path = Path.append path (Path.basic "test")
     val compile_cmd =
-      "\"$ISABELLE_OCAMLC\" -w pu -o " ^ File.bash_path compiled_path ^
-      " -I " ^ File.bash_path path ^
-      " nums.cma " ^ File.bash_path code_path ^ " " ^ File.bash_path driver_path
+      "\"$ISABELLE_ROOT/lib/scripts/ocamlexec\" ocamlfind ocamlopt -w pu -package zarith -linkpkg " ^
+      " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
+      File.bash_path code_path ^ " " ^ File.bash_path driver_path
 
     val run_cmd = File.bash_path compiled_path
   in
     {files = [(driver_path, driver)],
      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   end
 
 fun evaluate_in_ocaml ctxt =
-  evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLC, "ocamlc executable")) ocamlN ctxt
+  evaluate mk_driver_ocaml (SOME (ISABELLE_OPAM_ROOT, "ocaml opam environment")) ocamlN ctxt
 
 
 (* driver for GHC *)
 
 val ghcN = "GHC"