# HG changeset patch # User huffman # Date 1271796268 25200 # Node ID 2a4cec6bcae2cb775f1a0e708e4e7d5a5f394601 # Parent 95a3fac5dcaeedacb5dfe27b8ab173e9f4de2d88 replace many uses of Drule.export_without_context with Drule.zero_var_indexes diff -r 95a3fac5dcae -r 2a4cec6bcae2 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Apr 20 22:34:17 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Apr 20 13:44:28 2010 -0700 @@ -85,7 +85,7 @@ val (lub_take_thm, thy) = Specification.axiom ((lub_take_bind, []), lub_take_eqn) thy; in - (Drule.export_without_context lub_take_thm, thy) + (lub_take_thm, thy) end; fun add_axioms diff -r 95a3fac5dcae -r 2a4cec6bcae2 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Tue Apr 20 22:34:17 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Tue Apr 20 13:44:28 2010 -0700 @@ -200,7 +200,7 @@ val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy); in Library.foldr mk_ex (vs, conj) end; val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec')); - (* first 3 rules replace "y = UU \/ P" with "rep$y = UU \/ P" *) + (* first rules replace "y = UU \/ P" with "rep$y = UU \/ P" *) val tacs = [ rtac (iso_locale RS @{thm iso.casedist_rule}) 1, rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})], @@ -210,7 +210,7 @@ val exhaust = (nchotomy RS @{thm exh_casedist0}) |> rewrite_rule @{thms exh_casedists} - |> Drule.export_without_context; + |> Drule.zero_var_indexes; end; (* prove compactness rules for constructors *) diff -r 95a3fac5dcae -r 2a4cec6bcae2 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Apr 20 22:34:17 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Apr 20 13:44:28 2010 -0700 @@ -136,7 +136,7 @@ val rep_iso = #rep_inverse info; val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso]; in - Drule.export_without_context thm + Drule.zero_var_indexes thm end (******************************************************************************) @@ -201,7 +201,7 @@ (* register unfold theorems *) val (unfold_thms, thy) = - (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context)) + (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (mk_unfold_thms unfold_binds tuple_unfold_thm) thy; in ((proj_thms, unfold_thms), thy) @@ -349,7 +349,7 @@ val deflation_map_binds = dbinds |> map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map"); val (deflation_map_thms, thy) = thy |> - (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context)) + (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (conjuncts deflation_map_binds deflation_map_thm); (* register map functions in theory data *) @@ -519,7 +519,7 @@ fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy = let fun make thm = - Drule.export_without_context (thm OF [REP_eq, abs_def, rep_def]); + Drule.zero_var_indexes (thm OF [REP_eq, abs_def, rep_def]); val rep_iso_thm = make @{thm domain_rep_iso}; val abs_iso_thm = make @{thm domain_abs_iso}; val isodefl_thm = make @{thm isodefl_abs_rep}; @@ -607,7 +607,7 @@ val thmR = thm RS @{thm conjunct2}; in (n, thmL):: conjuncts ns thmR end; val (isodefl_thms, thy) = thy |> - (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context)) + (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (conjuncts isodefl_binds isodefl_thm); val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy; diff -r 95a3fac5dcae -r 2a4cec6bcae2 src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Apr 20 22:34:17 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Apr 20 13:44:28 2010 -0700 @@ -167,7 +167,7 @@ val rep_iso = #rep_inverse info; val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso]; in - Drule.export_without_context thm + Drule.zero_var_indexes thm end (******************************************************************************) @@ -359,15 +359,15 @@ in (n, thmL):: conjuncts ns thmR end; val (deflation_take_thms, thy) = fold_map (add_qualified_thm "deflation_take") - (map (apsnd Drule.export_without_context) + (map (apsnd Drule.zero_var_indexes) (conjuncts dbinds deflation_take_thm)) thy; (* prove strictness of take functions *) fun prove_take_strict (deflation_take, dbind) thy = let val take_strict_thm = - Drule.export_without_context - (@{thm deflation_strict} OF [deflation_take]); + Drule.zero_var_indexes + (@{thm deflation_strict} OF [deflation_take]); in add_qualified_thm "take_strict" (dbind, take_strict_thm) thy end; @@ -379,8 +379,8 @@ fun prove_take_take ((chain_take, deflation_take), dbind) thy = let val take_take_thm = - Drule.export_without_context - (@{thm deflation_chain_min} OF [chain_take, deflation_take]); + Drule.zero_var_indexes + (@{thm deflation_chain_min} OF [chain_take, deflation_take]); in add_qualified_thm "take_take" (dbind, take_take_thm) thy end; @@ -392,8 +392,8 @@ fun prove_take_below (deflation_take, dbind) thy = let val take_below_thm = - Drule.export_without_context - (@{thm deflation.below} OF [deflation_take]); + Drule.zero_var_indexes + (@{thm deflation.below} OF [deflation_take]); in add_qualified_thm "take_below" (dbind, take_below_thm) thy end; @@ -542,7 +542,7 @@ fun prove_reach_lemma ((chain_take, lub_take), dbind) thy = let val thm = - Drule.export_without_context + Drule.zero_var_indexes (@{thm lub_ID_reach} OF [chain_take, lub_take]); in add_qualified_thm "reach" (dbind, thm) thy @@ -575,7 +575,7 @@ else let fun prove_take_induct (chain_take, lub_take) = - Drule.export_without_context + Drule.zero_var_indexes (@{thm lub_ID_take_induct} OF [chain_take, lub_take]); val take_inducts = map prove_take_induct (chain_take_thms ~~ lub_take_thms); diff -r 95a3fac5dcae -r 2a4cec6bcae2 src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Tue Apr 20 22:34:17 2010 +0200 +++ b/src/HOLCF/Tools/pcpodef.ML Tue Apr 20 13:44:28 2010 -0700 @@ -91,7 +91,7 @@ val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy; (* transfer thms so that they will know about the new cpo instance *) val cpo_thms' = map (Thm.transfer thy) cpo_thms; - fun make thm = Drule.export_without_context (thm OF cpo_thms'); + fun make thm = Drule.zero_var_indexes (thm OF cpo_thms'); val cont_Rep = make @{thm typedef_cont_Rep}; val cont_Abs = make @{thm typedef_cont_Abs}; val lub = make @{thm typedef_lub}; @@ -133,7 +133,7 @@ val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1; val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy; val pcpo_thms' = map (Thm.transfer thy) pcpo_thms; - fun make thm = Drule.export_without_context (thm OF pcpo_thms'); + fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms'); val Rep_strict = make @{thm typedef_Rep_strict}; val Abs_strict = make @{thm typedef_Abs_strict}; val Rep_strict_iff = make @{thm typedef_Rep_strict_iff}; diff -r 95a3fac5dcae -r 2a4cec6bcae2 src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Tue Apr 20 22:34:17 2010 +0200 +++ b/src/HOLCF/Tools/repdef.ML Tue Apr 20 13:44:28 2010 -0700 @@ -141,7 +141,7 @@ |> Sign.add_path (Binding.name_of name) |> PureThy.add_thm ((Binding.prefix_name "REP_" name, - Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), []) + Drule.zero_var_indexes (@{thm typedef_REP} OF typedef_thms')), []) ||> Sign.restore_naming thy; val rep_info =