--- a/src/HOL/Hoare/hoare_tac.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Mon Jun 23 23:45:39 2008 +0200
@@ -72,8 +72,7 @@
(Free ("P",varsT --> boolT) $ mk_bodyC vars));
val small_Collect = mk_CollectC (Abs("x",varsT,
Free ("P",varsT --> boolT) $ Bound 0));
- val impl = implies $ (Mset_incl big_Collect) $
- (Mset_incl small_Collect);
+ val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
end;