theory stlc_codegen = stlc + ExecutableSet:

ML "reset Codegen.quiet_mode"

constdefs ta :: t
  "ta == 
  TmApp  (TmAbs ''x'' TyBool (TmVar ''x''))  TmTrue"

(* looks like codegen fails for nested datatypes ? *)

code_module Stlc_codegen file "stlc_codegen.ml" contains
(*is_v
tsubst_T
tsubst_t*)
E_tmp = "CCase ''l'' ''x'' TmTrue";
E_tmp = "TmTrue";
E_ta  = "TyBool(ta,_):E"

end