theory Scratch
  imports Main
begin

export_code 1 in SML file_prefix "hello"

generate_file "Pure.hs" = \<open>
  module Isabelle.Pure where
    allConst, impConst, eqConst :: String
    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
  \<close>

ML \<open>
Generated_Files.get_files \<^theory>
|> map #path
\<close>

end