--- a/src/HOL/Fun.thy Wed Dec 27 19:09:54 2006 +0100 +++ b/src/HOL/Fun.thy Wed Dec 27 19:09:55 2006 +0100 @@ -480,6 +480,9 @@ (SML infixl 5 "o") (Haskell infixr 9 ".") +code_const "id" + (Haskell "id") + subsection {* ML legacy bindings *}