# HG changeset patch
# User wenzelm
# Date 1540933716 -3600
# Node ID be8c70794375eee3a2b93bb2579fe0859295c8c4
# Parent  7062639cfdaa94fb3eed9b8a69b89df6262e08ca
tuned example;

diff -r 7062639cfdaa -r be8c70794375 NEWS
--- a/NEWS	Tue Oct 30 22:05:30 2018 +0100
+++ b/NEWS	Tue Oct 30 22:08:36 2018 +0100
@@ -93,14 +93,14 @@
 Haskell string literal. This allows to refer to Isabelle items robustly,
 e.g. via Isabelle/ML antiquotations or library operations. For example:
 
-ML \<open>
+ML_command \<open>
   GHC.read_source \<^context> \<open>
     allConst, impConst, eqConst :: String
     allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
     impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
     eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
   \<close>
-  |> File.write \<^path>\<open>consts.hs\<close>
+  |> writeln
 \<close>