theory Code
imports Main
begin

locale A =
fixes b :: 'b
and ba :: "'b \<Rightarrow> 'a :: linorder"
and baa :: "'b \<Rightarrow> 'a \<Rightarrow> 'a :: linorder"
assumes "baa b a = a"
begin

definition code :: "'a \<Rightarrow> 'a" where
  "code a = baa b a"

end

definition my_code where [code del]: "my_code \<equiv> \<lambda>a. A.code a (\<lambda>_. id)"

interpretation A as id "\<lambda>_. id" where "A.code as (\<lambda>_. id) = my_code as" sorry

export_code my_code in SML

end