--- a/src/HOL/BNF/Tools/bnf_def.ML Tue May 07 14:22:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Tue May 07 14:47:22 2013 +0200
@@ -662,7 +662,6 @@
val CB' = mk_bnf_T Bs' CA;
val CC' = mk_bnf_T Cs CA;
val CRs' = mk_bnf_T RTs CA;
- val CA'CB' = HOLogic.mk_prodT (CA', CB');
val bnf_map_AsAs = mk_bnf_map As' As';
val bnf_map_AsBs = mk_bnf_map As' Bs';
@@ -674,15 +673,14 @@
val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
val pre_names_lthy = lthy;
- val (((((((((((((((((((((((fs, gs), hs), p), (x, x')), (y, y')), (z, z')), zs), As),
+ val ((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), As),
As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
names_lthy) = pre_names_lthy
|> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
||>> mk_Frees "h" (map2 (curry (op -->)) As' Ts)
- ||>> yield_singleton (mk_Frees "p") CA'CB'
- ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "x") CA'
- ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "y") CB'
+ ||>> yield_singleton (mk_Frees "x") CA'
+ ||>> yield_singleton (mk_Frees "y") CB'
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "z") CRs'
||>> mk_Frees "z" As'
||>> mk_Frees "A" (map HOLogic.mk_setT As')
@@ -1022,7 +1020,7 @@
Goal.prove_sorry lthy [] []
(mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
HOLogic.eq_const CA'))
- (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms))
+ (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms)))
|> Thm.close_derivation
end;
@@ -1083,16 +1081,13 @@
val in_rel = Lazy.lazy mk_in_rel;
- val predicate2_cong = @{thm predicate2_cong};
- val mem_Collect_etc = @{thms fst_conv mem_Collect_eq prod.cases snd_conv};
-
fun mk_rel_flip () =
let
val rel_conversep_thm = Lazy.force rel_conversep;
val cts = map (SOME o certify lthy) Rs;
val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
in
- unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS predicate2_cong)
+ unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_cong})
|> singleton (Proof_Context.export names_lthy pre_names_lthy)
end;