src/Pure/Pure.thy

--- 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>