avoid dangling tfrees;
authorwenzelm
Sun May 20 21:12:23 2018 +0200 (21 months ago)
changeset 68236b4484ec4a8f7
parent 68235 a3bd410db5b2
child 68237 e7c85e2dc198
avoid dangling tfrees;
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun May 20 20:37:11 2018 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun May 20 21:12:23 2018 +0200
     1.3 @@ -518,7 +518,7 @@
     1.4      fun prove_reach_lemma ((chain_take, lub_take), dbind) thy =
     1.5        let
     1.6          val thm =
     1.7 -            Drule.zero_var_indexes
     1.8 +            Drule.export_without_context
     1.9                (@{thm lub_ID_reach} OF [chain_take, lub_take])
    1.10        in
    1.11          add_qualified_thm "reach" (dbind, thm) thy
    1.12 @@ -551,7 +551,7 @@
    1.13        else
    1.14          let
    1.15            fun prove_take_induct (chain_take, lub_take) =
    1.16 -              Drule.zero_var_indexes
    1.17 +              Drule.export_without_context
    1.18                  (@{thm lub_ID_take_induct} OF [chain_take, lub_take])
    1.19            val take_inducts =
    1.20                map prove_take_induct (chain_take_thms ~~ lub_take_thms)