889 "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null"}, |
889 "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null"}, |
890 evaluation_args = []}) |
890 evaluation_args = []}) |
891 #> Code_Target.set_printings (Type_Constructor ("fun", |
891 #> Code_Target.set_printings (Type_Constructor ("fun", |
892 [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))])) |
892 [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))])) |
893 #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names |
893 #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names |
894 #> fold (Code_Target.add_reserved target_SML) |
894 #> fold (Code_Target.add_reserved target_SML) [ |
895 ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*), |
895 "ref", (*rebinding is illegal*) |
896 "Fail", "div", "mod" (*standard infixes*), "IntInf"] |
896 "o", (*dictionary projections use it already*) |
|
897 "nil", (*predefined constructor*) |
|
898 "Fail", |
|
899 "div", "mod", (*standard infixes*) |
|
900 "IntInf"] |
897 #> fold (Code_Target.add_reserved target_OCaml) [ |
901 #> fold (Code_Target.add_reserved target_OCaml) [ |
898 "and", "as", "assert", "begin", "class", |
902 "and", "as", "assert", "begin", "class", |
899 "constraint", "do", "done", "downto", "else", "end", "exception", |
903 "constraint", "do", "done", "downto", "else", "end", "exception", |
900 "external", "false", "for", "fun", "function", "functor", "if", |
904 "external", "false", "for", "fun", "function", "functor", "if", |
901 "in", "include", "inherit", "initializer", "lazy", "let", "match", "method", |
905 "in", "include", "inherit", "initializer", "lazy", "let", "match", "method", |