--- a/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 16:26:48 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 16:38:20 2010 +0200
@@ -2,10 +2,4 @@
 imports Array Ref
 begin
 
-lemma crel_option_case:
-  assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
-  obtains "x = None" "crel n h h' r"
-        | y where "x = Some y" "crel (s y) h h' r" 
-  using assms unfolding crel_def by (auto split: option.splits)
-
 end