Added symmetric code_unfold-lemmas for null and is_none

--- a/src/HOL/List.thy	Thu Sep 26 11:41:01 2013 +0200
+++ b/src/HOL/List.thy	Thu Sep 26 13:37:33 2013 +0200
@@ -6002,7 +6002,8 @@
 
 lemma equal_Nil_null [code_unfold]:
   "HOL.equal xs [] \<longleftrightarrow> null xs"
-  by (simp add: equal eq_Nil_null)
+  "HOL.equal [] = null"
+  by (auto simp add: equal null_def)
 
 definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
   [code_abbrev]: "maps f xs = concat (map f xs)"

--- a/src/HOL/Option.thy	Thu Sep 26 11:41:01 2013 +0200
+++ b/src/HOL/Option.thy	Thu Sep 26 13:37:33 2013 +0200
@@ -187,7 +187,8 @@
 
 lemma [code_unfold]:
   "HOL.equal x None \<longleftrightarrow> is_none x"
-  by (simp add: equal is_none_def)
+  "HOL.equal None = is_none"
+  by (auto simp add: equal is_none_def)
 
 hide_const (open) is_none