Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid dangling tfrees;
authorwenzelm
Sun, 20 May 2018 21:12:23 +0200
changeset 68236 b4484ec4a8f7
parent 68235 a3bd410db5b2
child 68237 e7c85e2dc198
avoid dangling tfrees;
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle