# HG changeset patch
# User blanchet
# Date 1411051660 -7200
# Node ID ffc8669e46cf0ee00e667d8bf781b8b496379059
# Parent  149fb885dcd8ff58e15cc14c4e94ba75293312b4
made 'mk_pointfree' work again in local theories

diff -r 149fb885dcd8 -r ffc8669e46cf src/HOL/Tools/BNF/bnf_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_tactics.ML	Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Thu Sep 18 16:47:40 2014 +0200
@@ -50,15 +50,13 @@
 
 (*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
-  |> Drule.zero_var_indexes
-  |> Thm.prop_of
-  |> Logic.unvarify_global
-  |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
+  |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
   |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
   |> mk_Trueprop_eq
   |> (fn goal => Goal.prove_sorry ctxt [] [] goal
-    (K (rtac ext 1 THEN rtac @{thm comp_apply_eq} 1 THEN rtac thm 1)))
-  |> Drule.export_without_context
+    (K (rtac @{thm ext} 1 THEN
+        unfold_thms_tac ctxt ([o_apply, unfold_thms ctxt [o_apply] (mk_sym thm)]) THEN
+        rtac refl 1)))
   |> Thm.close_derivation;