src/HOL/List.thy

--- a/src/HOL/List.thy	Thu May 14 15:09:46 2009 +0200
+++ b/src/HOL/List.thy	Thu May 14 15:09:47 2009 +0200
@@ -3646,10 +3646,14 @@
 
 lemmas in_set_code [code unfold] = mem_iff [symmetric]
 
-lemma empty_null [code inline]:
+lemma empty_null:
   "xs = [] \<longleftrightarrow> null xs"
 by (cases xs) simp_all
 
+lemma [code inline]:
+  "eq_class.eq xs [] \<longleftrightarrow> null xs"
+by (simp add: eq empty_null)
+
 lemmas null_empty [code post] =
   empty_null [symmetric]