--- a/src/HOL/Tools/BNF/bnf_tactics.ML Wed Oct 26 20:59:36 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML Wed Oct 26 22:40:28 2016 +0200
@@ -17,7 +17,7 @@
val mk_rotate_eq_tac: Proof.context -> (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list ->
''a list -> int -> tactic
- val mk_pointfree: Proof.context -> thm -> thm
+ val mk_pointfree2: Proof.context -> thm -> thm
val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
val mk_Abs_inj_thm: thm -> thm
@@ -47,14 +47,13 @@
fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt o the_default [0];
-
(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
-fun mk_pointfree ctxt thm = thm
+fun mk_pointfree2 ctxt thm = thm
|> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
|> apply2 (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
|> mk_Trueprop_eq
|> (fn goal => Goal.prove_sorry ctxt [] [] goal
- (K (rtac ctxt @{thm ext} 1 THEN
+ (K (rtac ctxt ext 1 THEN
unfold_thms_tac ctxt ([o_apply, unfold_thms ctxt [o_apply] (mk_sym thm)]) THEN
rtac ctxt refl 1)))
|> Thm.close_derivation;
@@ -67,7 +66,6 @@
(Abs_inj_thm RS @{thm bijI'});
-
(* General tactic generators *)
(*applies assoc rule to the lhs of an equation as long as possible*)