# HG changeset patch
# User blanchet
# Date 1280834966 -7200
# Node ID c15dfe7bc077ead7ecc8046846eb7d592c90b4bb
# Parent  de6ef87e65b3c15851d1ad66b2dbc1400f7fde6c
fix newly introduced bug w.r.t. conditional equations

diff -r de6ef87e65b3 -r c15dfe7bc077 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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 =