--- a/src/Doc/Codegen/Inductive_Predicate.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Codegen/Inductive_Predicate.thy Fri Aug 12 17:53:55 2016 +0200
@@ -262,7 +262,7 @@
text \<open>
Further examples for compiling inductive predicates can be found in
- @{file "~~/src/HOL/Predicate_Compile_Examples/Examples.thy"}. There are
+ \<^file>\<open>~~/src/HOL/Predicate_Compile_Examples/Examples.thy\<close>. There are
also some examples in the Archive of Formal Proofs, notably in the
@{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
sessions.