src/HOL/ex/Records.thy

--- a/src/HOL/ex/Records.thy	Mon Apr 30 12:14:53 2012 +0200
+++ b/src/HOL/ex/Records.thy	Mon Apr 30 22:18:39 2012 +1000
@@ -324,4 +324,16 @@
 
 export_code foo1 foo3 foo5 foo10 checking SML
 
+text {*
+  Code generation can also be switched off, for instance for very large records
+*}
+
+declare [[record_codegen = false]]
+
+record not_so_large_record =
+  bar520 :: nat
+  bar521 :: "nat * nat"
+
+declare [[record_codegen = true]]
+
 end