fix newly introduced bug w.r.t. conditional equations

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 03 13:17:15 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 03 13:29:26 2010 +0200
@@ -1727,10 +1727,11 @@
 (** Axiom extraction/generation **)
 
 fun equationalize t =
-  case Logic.strip_imp_concl t of
-    @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ _) => t
-  | @{const Trueprop} $ t' =>
-    @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
+  case Logic.strip_horn t of
+    (_, @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ _)) => t
+  | (prems, @{const Trueprop} $ t') =>
+    Logic.list_implies (prems,
+                        @{const Trueprop} $ HOLogic.mk_eq (t', @{const True}))
   | _ => t
 
 fun pair_for_prop t =