src/HOL/Tools/BNF/bnf_tactics.ML

   val subst_asm_tac: Proof.context -> int list option -> thm list -> int -> tactic
 
   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
 
   val mk_map_comp_id_tac: Proof.context -> thm -> tactic

 
 (*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*)
 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;
 
 
 (* Theorems for open typedefs with UNIV as representing set *)
 
 fun mk_Abs_inj_thm inj = inj OF (replicate 2 @{thm UNIV_I});
 fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac ctxt surj THEN' etac ctxt exI) 1)
   (Abs_inj_thm RS @{thm bijI'});
-
 
 
 (* General tactic generators *)
 
 (*applies assoc rule to the lhs of an equation as long as possible*)