src/Pure/ML_Bootstrap.thy
changeset 76670 b04d45bebbc5
parent 68918 3a0db30e5d87
child 78728 72631efa3821
--- a/src/Pure/ML_Bootstrap.thy	Sat Dec 17 19:09:46 2022 +0100
+++ b/src/Pure/ML_Bootstrap.thy	Sat Dec 17 19:19:10 2022 +0100
@@ -8,8 +8,6 @@
 imports Pure
 begin
 
-external_file "$POLYML_EXE"
-
 ML \<open>
   #allStruct ML_Name_Space.global () |> List.app (fn (name, _) =>
     if member (op =) ML_Name_Space.hidden_structures name then