--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Tue Sep 04 13:06:41 2012 +0200
@@ -223,9 +223,7 @@
let
val comp_in = mk_in Asets comp_sets CCA;
val comp_in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
- val goal =
- fold_rev Logic.all Asets
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (comp_in, comp_in_alt)));
+ val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (comp_in, comp_in_alt));
in
Skip_Proof.prove lthy [] [] goal
(fn {context, ...} => mk_comp_in_alt_tac context comp_set_alt_thms)
@@ -346,8 +344,7 @@
let
val killN_in = mk_in Asets killN_sets T;
val killN_in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
- val goal =
- fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (killN_in, killN_in_alt)));
+ val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (killN_in, killN_in_alt));
in
Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation
end;
@@ -455,8 +452,7 @@
let
val liftN_in = mk_in Asets liftN_sets T;
val liftN_in_alt = mk_in (drop n Asets) bnf_sets T;
- val goal =
- fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (liftN_in, liftN_in_alt)))
+ val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (liftN_in, liftN_in_alt));
in
Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation
end;
@@ -541,9 +537,7 @@
let
val permute_in = mk_in Asets permute_sets T;
val permute_in_alt = mk_in (permute_rev Asets) bnf_sets T;
- val goal =
- fold_rev Logic.all Asets
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (permute_in, permute_in_alt)));
+ val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (permute_in, permute_in_alt));
in
Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
|> Thm.close_derivation