theory Example imports Executable_Set
begin

definition "foo (x::'a set) \<equiv> x \<subseteq> x"

export_code foo in SML file -  -- {* generated code is not type correct *}

setup {*
  Code.add_signature_cmd ("foo", "'a set \<Rightarrow> bool")
*}

export_code foo in SML file -  -- {* now it works *}


record 'a rec = field :: "'a set"

export_code field in SML file -  -- {* @{const field} gets type @{typ
  "('a, 'b) rec_ext_type \<Rightarrow> 'a \<Rightarrow> bool"} *}

setup {*
  Code.add_signature_cmd ("field", "('a, 'b) rec_ext_type \<Rightarrow> 'a set")
*}

export_code field in SML file -  -- {* now @{const field} has the right
  type, but the code is no longer type-correct (because the underlying
  record implementation is still using @{typ "'a \<Rightarrow> bool"}) *}

end