--- 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