src/Pure/Pure.thy

--- a/src/Pure/Pure.thy	Tue Nov 28 22:14:10 2017 +0100
+++ b/src/Pure/Pure.thy	Wed Nov 29 10:27:56 2017 +0100
@@ -120,8 +120,6 @@
       in () end)));
 \<close>
 
-external_file "$POLYML_EXE"
-
 
 subsection \<open>Embedded ML text\<close>