diff -r b933700f0384 -r 3d4953e88449 src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -106,7 +106,7 @@
   "fmsize (A p) = 4+ fmsize p"
   "fmsize p = 1"
   (* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p > 0"	
+lemma fmsize_pos: "fmsize p \<noteq> 0"
 by (induct p rule: fmsize.induct) simp_all
 
   (* Semantics of formulae (fm) *)
@@ -917,7 +917,7 @@
   "prep (Imp p q) = prep (Or (NOT p) q)"
   "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   "prep p = p"
-(hints simp add: fmsize_pos)
+(hints simp add: fmsize_pos neq0_conv[symmetric])
 lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
 by (induct p rule: prep.induct, auto)