--- a/src/HOL/IMPP/Hoare.ML	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/IMPP/Hoare.ML	Wed Dec 21 12:02:57 2005 +0100
@@ -220,6 +220,7 @@
 qed "MGF_complete";
 
 AddSEs WTs_elim_cases;
+AddIffs [not_None_eq];
 (* requires com_det, escape (i.e. hoare_derivs.conseq) *)
 Goal "state_not_singleton ==> \
 \ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}";