# HG changeset patch
# User wenzelm
# Date 1470995627 -7200
# Node ID 8e0148e1f5f49dfd635911ccbeaf56df2393191f
# Parent  256fc20716f2034358d937baac39faf128330e6f
tuned;

diff -r 256fc20716f2 -r 8e0148e1f5f4 src/Doc/Codegen/Evaluation.thy
--- a/src/Doc/Codegen/Evaluation.thy	Thu Aug 11 18:26:44 2016 +0200
+++ b/src/Doc/Codegen/Evaluation.thy	Fri Aug 12 11:53:47 2016 +0200
@@ -340,7 +340,7 @@
   For technical reasons it is sometimes necessary to separate
   generation and compilation of code which is supposed to be used in
   the system runtime.  For this @{command code_reflect} with an
-  optional @{text "file"} argument can be used:
+  optional \<^theory_text>\<open>file\<close> argument can be used:
 \<close>
 
 code_reflect %quote Rat