diff -r d80b2df54d31 -r a96320074298 src/Tools/SML/Examples.thy --- a/src/Tools/SML/Examples.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/Tools/SML/Examples.thy Sun Jan 06 15:04:34 2019 +0100 @@ -21,7 +21,7 @@ evaluates it for some arguments. \ -SML_file "factorial.sml" +SML_file \factorial.sml\ text \ The subsequent example illustrates the use of multiple \<^theory_text>\SML_file\ commands @@ -30,8 +30,8 @@ independently of the Isabelle/ML environment. \ -SML_file "Example.sig" -SML_file "Example.sml" +SML_file \Example.sig\ +SML_file \Example.sml\ text \