# HG changeset patch # User wenzelm # Date 1510158872 -3600 # Node ID 09fb749d1a1e34090b5e0f03b5c7a11daa142f4b # Parent 2288cc39b038a0c64ea35ed03608a8626604522f formal dependency on "poly" executable; diff -r 2288cc39b038 -r 09fb749d1a1e 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))); \ +external_file "$POLYML_EXE" + subsection \Embedded ML text\