--- a/src/Tools/Code/code_ml.ML Mon Aug 30 15:52:09 2010 +0900
+++ b/src/Tools/Code/code_ml.ML Mon Aug 30 09:28:02 2010 +0200
@@ -966,11 +966,11 @@
Code_Target.add_target
(target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
- make_command = fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure" } })
+ make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
#> Code_Target.add_target
(target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
- make_command = fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p } })
+ make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
#> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,