--- 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
--- 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 *)
--- 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;
--- 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);
--- 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};
--- 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 =