# HG changeset patch
# User wenzelm
# Date 1496223817 -7200
# Node ID e2c25346b1561cdc9cc2e0950ff44c86ab904903
# Parent  3bec939bd808c4f99970b461deaf82a0e8dbb510
more robust -- avoid race condition wrt. Haskell output in $ISABELLE_TMP/examples/

diff -r 3bec939bd808 -r e2c25346b156 src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Tue May 30 22:39:18 2017 +0200
+++ b/src/Doc/Codegen/Further.thy	Wed May 31 11:43:37 2017 +0200
@@ -48,7 +48,7 @@
   functions Fract
     "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
-  file "$ISABELLE_TMP/examples/rat.ML"
+  file "$ISABELLE_TMP/rat.ML"
 
 text \<open>
   \noindent This merely generates the referenced code to the given
diff -r 3bec939bd808 -r e2c25346b156 src/Doc/Codegen/Introduction.thy
--- a/src/Doc/Codegen/Introduction.thy	Tue May 30 22:39:18 2017 +0200
+++ b/src/Doc/Codegen/Introduction.thy	Wed May 31 11:43:37 2017 +0200
@@ -70,7 +70,7 @@
 text \<open>\noindent Then we can generate code e.g.~for @{text SML} as follows:\<close>
 
 export_code %quote empty dequeue enqueue in SML
-  module_name Example file "$ISABELLE_TMP/examples/example.ML"
+  module_name Example file "$ISABELLE_TMP/example.ML"
 
 text \<open>\noindent resulting in the following code:\<close>