src/HOL/ex/Records.thy

--- a/src/HOL/ex/Records.thy	Wed Nov 11 15:10:26 2009 +0100
+++ b/src/HOL/ex/Records.thy	Wed Nov 11 15:10:29 2009 +0100
@@ -334,4 +334,8 @@
   done
 
 
+subsection {* Some code generation *}
+
+export_code foo1 foo3 foo5 foo10 foo11 in SML file -
+
 end