1.1 --- a/src/Tools/Code/code_ml.ML	Wed Feb 13 13:38:52 2013 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Wed Feb 13 13:38:52 2013 +0100
     1.3 @@ -833,7 +833,7 @@
     1.4        check = { env_var = "ISABELLE_PROCESS",
     1.5          make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
     1.6          make_command = fn _ =>
     1.7 -          "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 0' Pure" } })
     1.8 +          "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
     1.9    #> Code_Target.add_target
    1.10      (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
    1.11        check = { env_var = "ISABELLE_OCAML",

     2.1 --- a/src/Tools/Code/lib/Tools/codegen	Wed Feb 13 13:38:52 2013 +0100
     2.2 +++ b/src/Tools/Code/lib/Tools/codegen	Wed Feb 13 13:38:52 2013 +0100
     2.3 @@ -52,7 +52,7 @@
     2.4  
     2.5  FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \
     2.6    (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
     2.7 -  handle _ => Posix.Process.exit 0w1;"
     2.8 +  handle _ => exit 1;"
     2.9  
    2.10  ACTUAL_CMD="val thyname = \"$THYNAME\"; \
    2.11    val _ = quick_and_dirty := $QUICK_AND_DIRTY; \