src/Tools/Code/code_ml.ML
changeset 38863 9070a7c356c9
parent 38784 3b4d63ab03c4
child 38910 6af1d8673cbf
     1.1 --- a/src/Tools/Code/code_ml.ML	Mon Aug 30 15:52:09 2010 +0900
     1.2 +++ b/src/Tools/Code/code_ml.ML	Mon Aug 30 09:28:02 2010 +0200
     1.3 @@ -966,11 +966,11 @@
     1.4    Code_Target.add_target
     1.5      (target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
     1.6        check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
     1.7 -        make_command = fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure" } })
     1.8 +        make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
     1.9    #> Code_Target.add_target
    1.10      (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
    1.11        check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
    1.12 -        make_command = fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p } })
    1.13 +        make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
    1.14    #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    1.15        brackify_infix (1, R) fxy (
    1.16          print_typ (INFX (1, X)) ty1,