# HG changeset patch
# User wenzelm
# Date 1526843543 -7200
# Node ID b4484ec4a8f78d155dddd7aeab23a83af693fa74
# Parent  a3bd410db5b21ed1397862eb4bf0599f2d67a1de
avoid dangling tfrees;

diff -r a3bd410db5b2 -r b4484ec4a8f7 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun May 20 20:37:11 2018 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun May 20 21:12:23 2018 +0200
@@ -518,7 +518,7 @@
     fun prove_reach_lemma ((chain_take, lub_take), dbind) thy =
       let
         val thm =
-            Drule.zero_var_indexes
+            Drule.export_without_context
               (@{thm lub_ID_reach} OF [chain_take, lub_take])
       in
         add_qualified_thm "reach" (dbind, thm) thy
@@ -551,7 +551,7 @@
       else
         let
           fun prove_take_induct (chain_take, lub_take) =
-              Drule.zero_var_indexes
+              Drule.export_without_context
                 (@{thm lub_ID_take_induct} OF [chain_take, lub_take])
           val take_inducts =
               map prove_take_induct (chain_take_thms ~~ lub_take_thms)