--- a/src/Doc/Codegen/Evaluation.thy Fri Jan 09 21:20:07 2015 +0100
+++ b/src/Doc/Codegen/Evaluation.thy Sat Jan 10 10:24:30 2015 +0100
@@ -326,7 +326,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 "examples/rat.ML"
+ file "$ISABELLE_TMP/examples/rat.ML"
text {*
\noindent This merely generates the referenced code to the given