| changeset 24348 | c708ea5b109a |
| parent 24249 | 1f60b45c5f97 |
| child 24423 | ae9cd0e92423 |
--- a/src/HOL/Lambda/WeakNorm.thy Mon Aug 20 18:07:31 2007 +0200 +++ b/src/HOL/Lambda/WeakNorm.thy Mon Aug 20 18:07:49 2007 +0200 @@ -581,7 +581,7 @@ int :: "nat \<Rightarrow> int" where "int \<equiv> of_nat" -code_gen type_NF nat int in SML module_name Norm +export_code type_NF nat int in SML module_name Norm ML {* val nat_of_int = Norm.nat o IntInf.fromInt;