--- a/src/HOL/Enum.thy Thu Jan 26 10:59:47 2012 +0100
+++ b/src/HOL/Enum.thy Thu Jan 26 12:03:35 2012 +0100
@@ -777,6 +777,7 @@
qed
code_abort enum_the
+code_const enum_the (Eval "(fn p => raise Match)")
subsection {* Further operations on finite types *}