--- a/src/Pure/Pure.thy Wed Nov 08 11:53:45 2017 +0100 +++ b/src/Pure/Pure.thy Wed Nov 08 17:34:32 2017 +0100 @@ -120,6 +120,8 @@ in () end))); \<close> +external_file "$POLYML_EXE" + subsection \<open>Embedded ML text\<close>