src/Doc/Codegen/Introduction.thy

   by (cases xs) (simp_all split: list.splits) (*>*)
 
 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>
 
 text %quotetypewriter \<open>
   @{code_stmts empty enqueue dequeue (SML)}