--- 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 =