# HG changeset patch
# User wenzelm
# Date 1565111232 -7200
# Node ID 2353966954011ff5d30a2b3d1a894f8aac81000c
# Parent  9179e7a98196df46dfb6e2e158b243a37f33a660
more careful treatment of implicit context;

diff -r 9179e7a98196 -r 235396695401 src/ZF/Datatype.thy
--- 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)
diff -r 9179e7a98196 -r 235396695401 src/ZF/Tools/datatype_package.ML
--- 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
diff -r 9179e7a98196 -r 235396695401 src/ZF/Tools/induct_tacs.ML
--- 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
diff -r 9179e7a98196 -r 235396695401 src/ZF/Tools/primrec_package.ML
--- 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)