--- a/src/ZF/Datatype.thy Tue Aug 06 17:26:40 2019 +0200
+++ b/src/ZF/Datatype.thy Tue Aug 06 19:07:12 2019 +0200
@@ -97,7 +97,8 @@
val goal = Logic.mk_equals (old, new)
val thm = Goal.prove ctxt [] [] goal
(fn _ => resolve_tac ctxt @{thms iff_reflection} 1 THEN
- simp_tac (put_simpset datatype_ss ctxt addsimps #free_iffs lcon_info) 1)
+ simp_tac (put_simpset datatype_ss ctxt addsimps
+ (map (Thm.transfer thy) (#free_iffs lcon_info))) 1)
handle ERROR msg =>
(warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal);
raise Match)
--- a/src/ZF/Tools/datatype_package.ML Tue Aug 06 17:26:40 2019 +0200
+++ b/src/ZF/Tools/datatype_package.ML Tue Aug 06 19:07:12 2019 +0200
@@ -369,19 +369,20 @@
val dt_info =
{inductive = true,
constructors = constructors,
- rec_rewrites = recursor_eqns,
- case_rewrites = case_eqns,
- induct = induct,
- mutual_induct = mutual_induct,
- exhaustion = elim};
+ rec_rewrites = map Thm.trim_context recursor_eqns,
+ case_rewrites = map Thm.trim_context case_eqns,
+ induct = Thm.trim_context induct,
+ mutual_induct = Thm.trim_context mutual_induct,
+ exhaustion = Thm.trim_context elim};
val con_info =
{big_rec_name = big_rec_name,
constructors = constructors,
(*let primrec handle definition by cases*)
- free_iffs = free_iffs,
- rec_rewrites = (case recursor_eqns of
- [] => case_eqns | _ => recursor_eqns)};
+ free_iffs = map Thm.trim_context free_iffs,
+ rec_rewrites =
+ (case recursor_eqns of [] => case_eqns | _ => recursor_eqns)
+ |> map Thm.trim_context};
(*associate with each constructor the datatype name and rewrites*)
val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
--- a/src/ZF/Tools/induct_tacs.ML Tue Aug 06 17:26:40 2019 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Tue Aug 06 19:07:12 2019 +0200
@@ -96,8 +96,9 @@
val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i NONE state
val tn = find_tname ctxt' var (map Thm.term_of asms)
val rule =
- if exh then #exhaustion (datatype_info thy tn)
- else #induct (datatype_info thy tn)
+ datatype_info thy tn
+ |> (if exh then #exhaustion else #induct)
+ |> Thm.transfer thy;
val (Const(\<^const_name>\<open>mem\<close>,_) $ Var(ixn,_) $ _) =
(case Thm.prems_of rule of
[] => error "induction is not available for this datatype"
@@ -136,11 +137,11 @@
val dt_info =
{inductive = true,
constructors = constructors,
- rec_rewrites = recursor_eqns,
- case_rewrites = case_eqns,
- induct = induct,
- mutual_induct = @{thm TrueI}, (*No need for mutual induction*)
- exhaustion = elim};
+ rec_rewrites = map Thm.trim_context recursor_eqns,
+ case_rewrites = map Thm.trim_context case_eqns,
+ induct = Thm.trim_context induct,
+ mutual_induct = Thm.trim_context @{thm TrueI}, (*No need for mutual induction*)
+ exhaustion = Thm.trim_context elim};
val con_info =
{big_rec_name = big_rec_name,
@@ -149,8 +150,9 @@
free_iffs = [], (*thus we expect the necessary freeness rewrites
to be in the simpset already, as is the case for
Nat and disjoint sum*)
- rec_rewrites = (case recursor_eqns of
- [] => case_eqns | _ => recursor_eqns)};
+ rec_rewrites =
+ (case recursor_eqns of [] => case_eqns | _ => recursor_eqns)
+ |> map Thm.trim_context};
(*associate with each constructor the datatype name and rewrites*)
val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
--- a/src/ZF/Tools/primrec_package.ML Tue Aug 06 17:26:40 2019 +0200
+++ b/src/ZF/Tools/primrec_package.ML Tue Aug 06 19:07:12 2019 +0200
@@ -172,7 +172,7 @@
|> Sign.add_path (Long_Name.base_name fname)
|> Global_Theory.add_defs false [Thm.no_attributes (apfst Binding.name def)];
- val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
+ val rewrites = def_thm :: map (mk_meta_eq o Thm.transfer thy1) (#rec_rewrites con_info)
val eqn_thms =
eqn_terms |> map (fn t =>
Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)