src/Pure/Pure.thy
changeset 67034 09fb749d1a1e
parent 67013 335a7dce7cb3
child 67105 05ff3e6dbbce
equal deleted inserted replaced
67033:2288cc39b038 67034:09fb749d1a1e
   118         val path = Path.explode s;
   118         val path = Path.explode s;
   119         val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
   119         val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
   120       in () end)));
   120       in () end)));
   121 \<close>
   121 \<close>
   122 
   122 
       
   123 external_file "$POLYML_EXE"
       
   124 
   123 
   125 
   124 subsection \<open>Embedded ML text\<close>
   126 subsection \<open>Embedded ML text\<close>
   125 
   127 
   126 ML \<open>
   128 ML \<open>
   127 local
   129 local