# HG changeset patch
# User wenzelm
# Date 1457044402 -3600
# Node ID 93fa1efc7219c3b61b5de5e4c01fe0c775df5576
# Parent  77a5f21c449b0a18d4de8a80bf6d11e6ebc9562b
simplified;

diff -r 77a5f21c449b -r 93fa1efc7219 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Thu Mar 03 22:24:58 2016 +0100
+++ b/src/Doc/System/Basics.thy	Thu Mar 03 23:33:22 2016 +0100
@@ -369,7 +369,7 @@
   The next example demonstrates batch execution of Isabelle. We retrieve the
   \<^verbatim>\<open>Main\<close> theory value from the theory loader within ML (observe the delicate
   quoting rules for the Bash shell vs.\ ML):
-  @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main";' -q HOL\<close>}
+  @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' -q HOL\<close>}
 
   Note that the output text will be interspersed with additional junk messages
   by the ML runtime environment.
diff -r 77a5f21c449b -r 93fa1efc7219 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Mar 03 22:24:58 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Mar 03 23:33:22 2016 +0100
@@ -159,7 +159,7 @@
 
 my $cmd =
   "\"$ENV{'ISABELLE_PROCESS'}\" " .
-  "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;' -q $mirabelle_logic" .
+  "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\"' -q $mirabelle_logic" .
   $quiet;
 my $result = system "bash", "-c", $cmd;
 
diff -r 77a5f21c449b -r 93fa1efc7219 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Mar 03 22:24:58 2016 +0100
+++ b/src/Tools/Code/code_ml.ML	Thu Mar 03 23:33:22 2016 +0100
@@ -869,7 +869,7 @@
       check = { env_var = "ISABELLE_PROCESS",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
         make_command = fn _ =>
-          "\"$ISABELLE_PROCESS\" -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
+          "\"$ISABELLE_PROCESS\" -q -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
   #> Code_Target.add_language
     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
       check = { env_var = "ISABELLE_OCAML",