src/HOL/Datatype.thy

--- a/src/HOL/Datatype.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Datatype.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -726,7 +726,7 @@
 subsubsection {* Code generator setup *}
 
 definition
-  is_none :: "'a option \<Rightarrow> bool"
+  is_none :: "'a option \<Rightarrow> bool" where
   is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
 
 lemma is_none_code [code]: