src/HOL/IMP/Live.thy

--- a/src/HOL/IMP/Live.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Live.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -153,7 +153,6 @@
     where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
     by auto
   with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
-    (* FIXME why does s/h fail here? *)
 qed
 
 corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'"