merged
authorwenzelm
Tue, 06 Aug 2019 20:52:06 +0200
changeset 70662 5c1b2f616d15
parent 70654 8406a2c296e0 (current diff)
parent 70661 98b6da301e13 (diff)
child 70663 90acc6ce5beb
merged
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Aug 06 18:04:06 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Aug 06 20:52:06 2019 +0200
@@ -624,7 +624,7 @@
   let
     fun collect (data : Lifting_Info.quotient) l =
       if is_some (#pcr_info data)
-      then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l)
+      then ((Thm.symmetric o safe_mk_meta_eq o Thm.transfer' ctxt o #pcr_cr_eq o the o #pcr_info) data :: l)
       else l
     val table = Lifting_Info.get_quotients ctxt
   in
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Tue Aug 06 18:04:06 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Tue Aug 06 20:52:06 2019 +0200
@@ -185,7 +185,7 @@
     val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm
     val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl
     val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs
-    val minfo = {rel_quot_thm = rel_quot_thm}
+    val minfo = {rel_quot_thm = Thm.trim_context rel_quot_thm}
   in
     Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) context
   end
@@ -218,7 +218,9 @@
 fun transform_quotient phi {quot_thm, pcr_info} =
   {quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info}
 
-fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name
+fun lookup_quotients ctxt type_name =
+  Symtab.lookup (get_quotients ctxt) type_name
+  |> Option.map (transform_quotient (Morphism.transfer_morphism' ctxt))
 
 fun lookup_quot_thm_quotients ctxt quot_thm =
   let
@@ -232,7 +234,8 @@
   end
 
 fun update_quotients type_name qinfo context =
-  Data.map (map_quotients (Symtab.update (type_name, qinfo))) context
+  let val qinfo' = transform_quotient Morphism.trim_context_morphism qinfo
+  in Data.map (map_quotients (Symtab.update (type_name, qinfo'))) context end
 
 fun delete_quotients quot_thm context =
   let
@@ -292,9 +295,13 @@
 
 (* info about reflexivity rules *)
 
-val get_reflexivity_rules = Item_Net.content o get_reflexivity_rules' o Context.Proof
+fun get_reflexivity_rules ctxt =
+  Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt))
+  |> map (Thm.transfer' ctxt)
 
-fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
+fun add_reflexivity_rule thm =
+  Data.map (map_reflexivity_rules (Item_Net.update (Thm.trim_context thm)))
+
 val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule
 
 
@@ -360,16 +367,19 @@
 
 fun add_reflexivity_rules mono_rule context =
   let
-    fun find_eq_rule thm ctxt =
+    val ctxt = Context.proof_of context
+    val thy = Context.theory_of context
+
+    fun find_eq_rule thm =
       let
-        val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm;
-        val rules = Item_Net.retrieve (Transfer.get_relator_eq_item_net ctxt) concl_rhs;
+        val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm
+        val rules = Transfer.retrieve_relator_eq ctxt concl_rhs
       in
-        find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs,
-          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) thm)) rules
+        find_first (fn th => Pattern.matches thy (concl_rhs,
+          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) th)) rules
       end
 
-    val eq_rule = find_eq_rule mono_rule (Context.proof_of context);
+    val eq_rule = find_eq_rule mono_rule;
     val eq_rule = if is_some eq_rule then the eq_rule else error
       "No corresponding rule that the relator preserves equality was found."
   in
@@ -505,13 +515,17 @@
     end
 end
 
-fun get_distr_rules_raw context = Symtab.fold
-  (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules)
+fun get_distr_rules_raw context =
+  Symtab.fold (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules =>
+      pos_distr_rules @ neg_distr_rules @ rules)
     (get_relator_distr_data' context) []
+  |> map (Thm.transfer'' context)
 
-fun get_mono_rules_raw context = Symtab.fold
-  (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules)
+fun get_mono_rules_raw context =
+  Symtab.fold (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules =>
+      [pos_mono_rule, neg_mono_rule] @ rules)
     (get_relator_distr_data' context) []
+  |> map (Thm.transfer'' context)
 
 val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data
 
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 06 18:04:06 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 06 20:52:06 2019 +0200
@@ -426,10 +426,10 @@
         thm |> Thm.cprop_of |> Drule.strip_imp_concl
         |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
       val pcrel_def = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) pcrel_def
-      val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
+      val thm' = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
         handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
     in
-      rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm
+      rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm'
     end
 
   fun reduce_Domainp ctxt rules thm =
--- a/src/HOL/Tools/Transfer/transfer.ML	Tue Aug 06 18:04:06 2019 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Aug 06 20:52:06 2019 +0200
@@ -22,16 +22,16 @@
   val fold_relator_eqs_conv: Proof.context -> conv
   val unfold_relator_eqs_conv: Proof.context -> conv
   val get_transfer_raw: Proof.context -> thm list
-  val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
   val get_relator_eq: Proof.context -> thm list
+  val retrieve_relator_eq: Proof.context -> term -> thm list
   val get_sym_relator_eq: Proof.context -> thm list
   val get_relator_eq_raw: Proof.context -> thm list
   val get_relator_domain: Proof.context -> thm list
   val morph_pred_data: morphism -> pred_data -> pred_data
   val lookup_pred_data: Proof.context -> string -> pred_data option
   val update_pred_data: string -> pred_data -> Context.generic -> Context.generic
-  val get_compound_lhs: Proof.context -> (term * thm) Item_Net.T
-  val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T
+  val is_compound_lhs: Proof.context -> term -> bool
+  val is_compound_rhs: Proof.context -> term -> bool
   val transfer_add: attribute
   val transfer_del: attribute
   val transfer_raw_add: thm -> Context.generic -> Context.generic
@@ -67,7 +67,7 @@
 val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
   o HOLogic.dest_Trueprop o Thm.concl_of);
 
-datatype pred_data = PRED_DATA of {pred_def:thm, rel_eq_onp: thm, pred_simps: thm list}
+datatype pred_data = PRED_DATA of {pred_def: thm, rel_eq_onp: thm, pred_simps: thm list}
 
 fun mk_pred_data pred_def rel_eq_onp pred_simps = PRED_DATA {pred_def = pred_def, 
   rel_eq_onp = rel_eq_onp, pred_simps = pred_simps}
@@ -124,25 +124,32 @@
       pred_data = Symtab.merge (K true) (pd1, pd2) }
 )
 
-val get_transfer_raw = Item_Net.content o #transfer_raw o Data.get o Context.Proof
+fun get_net_content f ctxt =
+  Item_Net.content (f (Data.get (Context.Proof ctxt)))
+  |> map (Thm.transfer' ctxt)
+
+val get_transfer_raw = get_net_content #transfer_raw
 
 val get_known_frees = #known_frees o Data.get o Context.Proof
 
-val get_compound_lhs = #compound_lhs o Data.get o Context.Proof
+fun is_compound f ctxt t =
+  Item_Net.retrieve (f (Data.get (Context.Proof ctxt))) t
+  |> exists (fn (pat, _) => Pattern.matches (Proof_Context.theory_of ctxt) (pat, t));
 
-val get_compound_rhs = #compound_rhs o Data.get o Context.Proof
+val is_compound_lhs = is_compound #compound_lhs
+val is_compound_rhs = is_compound #compound_rhs
 
-val get_relator_eq_item_net = #relator_eq o Data.get o Context.Proof
+val get_relator_eq = get_net_content #relator_eq #> map safe_mk_meta_eq
 
-val get_relator_eq =
-  map safe_mk_meta_eq o Item_Net.content o #relator_eq o Data.get o Context.Proof
+fun retrieve_relator_eq ctxt t =
+  Item_Net.retrieve (#relator_eq (Data.get (Context.Proof ctxt))) t
+  |> map (Thm.transfer' ctxt)
 
-val get_sym_relator_eq =
-  map (Thm.symmetric o safe_mk_meta_eq) o Item_Net.content o #relator_eq o Data.get o Context.Proof
+val get_sym_relator_eq = get_net_content #relator_eq #> map (safe_mk_meta_eq #> Thm.symmetric)
 
-val get_relator_eq_raw = Item_Net.content o #relator_eq_raw o Data.get o Context.Proof
+val get_relator_eq_raw = get_net_content #relator_eq_raw
 
-val get_relator_domain = Item_Net.content o #relator_domain o Data.get o Context.Proof
+val get_relator_domain = get_net_content #relator_domain
 
 val get_pred_data = #pred_data o Data.get o Context.Proof
 
@@ -167,19 +174,20 @@
 fun map_relator_domain f = map_data I I I I I I f I
 fun map_pred_data      f = map_data I I I I I I I f
 
-fun add_transfer_thm thm = Data.map
-  (map_transfer_raw (Item_Net.update thm) o
-   map_compound_lhs
-     (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
-        Const (\<^const_name>\<open>Rel\<close>, _) $ _ $ (lhs as (_ $ _)) $ _ =>
-          Item_Net.update (lhs, thm)
-      | _ => I) o
-   map_compound_rhs
-     (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
-        Const (\<^const_name>\<open>Rel\<close>, _) $ _ $ _ $ (rhs as (_ $ _)) =>
-          Item_Net.update (rhs, thm)
-      | _ => I) o
-   map_known_frees (Term.add_frees (Thm.concl_of thm)))
+val add_transfer_thm =
+  Thm.trim_context #> (fn thm => Data.map
+    (map_transfer_raw (Item_Net.update thm) o
+     map_compound_lhs
+       (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
+          Const (\<^const_name>\<open>Rel\<close>, _) $ _ $ (lhs as (_ $ _)) $ _ =>
+            Item_Net.update (lhs, thm)
+        | _ => I) o
+     map_compound_rhs
+       (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
+          Const (\<^const_name>\<open>Rel\<close>, _) $ _ $ _ $ (rhs as (_ $ _)) =>
+            Item_Net.update (rhs, thm)
+        | _ => I) o
+     map_known_frees (Term.add_frees (Thm.concl_of thm))))
 
 fun del_transfer_thm thm = Data.map
   (map_transfer_raw (Item_Net.remove thm) o
@@ -560,16 +568,9 @@
     map_filter f (Symtab.dest tab)
   end
 
-fun retrieve_terms t net = map fst (Item_Net.retrieve net t)
-
-fun matches_list ctxt term =
-  is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term))
-
 fun transfer_rule_of_term ctxt equiv t =
   let
-    val compound_rhs = get_compound_rhs ctxt
-    fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t
-    val s = skeleton is_rhs ctxt t
+    val s = skeleton (is_compound_rhs ctxt) ctxt t
     val frees = map fst (Term.add_frees s [])
     val tfrees = map fst (Term.add_tfrees s [])
     fun prep a = "R" ^ Library.unprefix "'" a
@@ -590,9 +591,7 @@
 
 fun transfer_rule_of_lhs ctxt t =
   let
-    val compound_lhs = get_compound_lhs ctxt
-    fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t
-    val s = skeleton is_lhs ctxt t
+    val s = skeleton (is_compound_lhs ctxt) ctxt t
     val frees = map fst (Term.add_frees s [])
     val tfrees = map fst (Term.add_tfrees s [])
     fun prep a = "R" ^ Library.unprefix "'" a
@@ -853,10 +852,12 @@
   Theory.setup
     let
       val name = \<^binding>\<open>relator_eq\<close>
-      fun add_thm thm context = context
-        |> Data.map (map_relator_eq (Item_Net.update thm))
+      fun add_thm thm context =
+        context
+        |> Data.map (map_relator_eq (Item_Net.update (Thm.trim_context thm)))
         |> Data.map (map_relator_eq_raw
-            (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
+            (Item_Net.update
+              (Thm.trim_context (abstract_equalities_relator_eq (Context.proof_of context) thm))))
       fun del_thm thm context = context
         |> Data.map (map_relator_eq (Item_Net.remove thm))
         |> Data.map (map_relator_eq_raw
@@ -876,15 +877,21 @@
       val name = \<^binding>\<open>relator_domain\<close>
       fun add_thm thm context =
         let
-          val thm = abstract_domains_relator_domain (Context.proof_of context) thm
+          val thm' = thm
+            |> abstract_domains_relator_domain (Context.proof_of context)
+            |> Thm.trim_context
         in
-          context |> Data.map (map_relator_domain (Item_Net.update thm)) |> add_transfer_domain_thm thm
+          context
+          |> Data.map (map_relator_domain (Item_Net.update thm'))
+          |> add_transfer_domain_thm thm'
         end
       fun del_thm thm context =
         let
-          val thm = abstract_domains_relator_domain (Context.proof_of context) thm
+          val thm' = abstract_domains_relator_domain (Context.proof_of context) thm
         in
-          context |> Data.map (map_relator_domain (Item_Net.remove thm)) |> del_transfer_domain_thm thm
+          context
+          |> Data.map (map_relator_domain (Item_Net.remove thm'))
+          |> del_transfer_domain_thm thm'
         end
       val add = Thm.declaration_attribute add_thm
       val del = Thm.declaration_attribute del_thm
--- a/src/Pure/Isar/object_logic.ML	Tue Aug 06 18:04:06 2019 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Aug 06 20:52:06 2019 +0200
@@ -171,8 +171,9 @@
 
 (* maintain rules *)
 
-val get_atomize = #1 o #atomize_rulify o get_data;
-val get_rulify = #2 o #atomize_rulify o get_data;
+fun get_atomize_rulify f ctxt = map (Thm.transfer' ctxt) (f (#atomize_rulify (get_data ctxt)));
+val get_atomize = get_atomize_rulify #1;
+val get_rulify = get_atomize_rulify #2;
 
 fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
   (base_sort, judgment, (Thm.add_thm (Thm.trim_context th) atomize, rulify)));
--- a/src/Pure/drule.ML	Tue Aug 06 18:04:06 2019 +0200
+++ b/src/Pure/drule.ML	Tue Aug 06 20:52:06 2019 +0200
@@ -281,7 +281,8 @@
 (*Resolution: multiple arguments, multiple results*)
 local
   fun res opt_ctxt th i rule =
-    Thm.biresolution opt_ctxt false [(false, th)] i rule handle THM _ => Seq.empty;
+    (Thm.biresolution opt_ctxt false [(false, th)] i rule handle THM _ => Seq.empty)
+    |> Seq.map Thm.solve_constraints;
 
   fun multi_res _ _ [] rule = Seq.single rule
     | multi_res opt_ctxt i (th :: ths) rule =
@@ -297,14 +298,14 @@
   let
     val resolve = Thm.biresolution NONE false (map (pair false) thas) i
     fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
-  in maps resb thbs end;
+  in maps resb thbs |> map Thm.solve_constraints end;
 
 fun thas RL thbs = thas RLN (1, thbs);
 
 (*Isar-style multi-resolution*)
 fun bottom_rl OF rls =
   (case Seq.chop 2 (multi_resolve NONE rls bottom_rl) of
-    ([th], _) => th
+    ([th], _) => Thm.solve_constraints th
   | ([], _) => raise THM ("OF: no unifiers", 0, bottom_rl :: rls)
   | _ => raise THM ("OF: multiple unifiers", 0, bottom_rl :: rls));
 
@@ -318,7 +319,8 @@
 fun compose (tha, i, thb) =
   Thm.bicompose NONE {flatten = true, match = false, incremented = false} (false, tha, 0) i thb
   |> Seq.list_of |> distinct Thm.eq_thm
-  |> (fn [th] => th | _ => raise THM ("compose: unique result expected", i, [tha, thb]));
+  |> (fn [th] => Thm.solve_constraints th
+       | _ => raise THM ("compose: unique result expected", i, [tha, thb]));
 
 
 (** theorem equality **)
@@ -695,7 +697,7 @@
   Thm.bicompose NONE {flatten = true, match = false, incremented = incremented}
     (false, th1, 0) 1 th2
   |> Seq.list_of |> distinct Thm.eq_thm
-  |> (fn [th] => th | _ => raise THM ("COMP", 1, [th1, th2]));
+  |> (fn [th] => Thm.solve_constraints th | _ => raise THM ("COMP", 1, [th1, th2]));
 
 in
 
@@ -709,7 +711,7 @@
   (case distinct Thm.eq_thm (Seq.list_of
       (Thm.bicompose NONE {flatten = false, match = false, incremented = true}
         (false, th, n) i (incr_indexes th rule))) of
-    [th'] => th'
+    [th'] => Thm.solve_constraints th'
   | [] => raise THM ("comp_no_flatten", i, [th, rule])
   | _ => raise THM ("comp_no_flatten: unique result expected", i, [th, rule]));
 
--- a/src/Pure/raw_simplifier.ML	Tue Aug 06 18:04:06 2019 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Aug 06 20:52:06 2019 +0200
@@ -533,7 +533,9 @@
       if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (Thm.term_of elhs)
       then mk_eq_True ctxt (thm, name)
       else rrule_eq_True ctxt thm name lhs elhs rhs thm
-  end;
+  end |> map (fn {thm, name, lhs, elhs, perm} =>
+    {thm = Thm.trim_context thm, name = name, lhs = lhs,
+      elhs = Thm.trim_context_cterm elhs, perm = perm});
 
 fun orient_rrule ctxt (thm, name) =
   let
@@ -690,8 +692,7 @@
         raise SIMPLIFIER ("Congruence must start with a constant", [thm]);
       val (xs, _) = congs;
       val xs' = filter_out (fn (x : cong_name, _) => x = a) xs;
-      val weak' = xs' |> map_filter (fn (a, thm) =>
-        if is_full_cong thm then NONE else SOME a);
+      val weak' = xs' |> map_filter (fn (a, th) => if is_full_cong th then NONE else SOME a);
     in ((xs', weak'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end);
 
 fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt;
@@ -1351,7 +1352,11 @@
     val _ =
       cond_tracing ctxt (fn () =>
         print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (Thm.term_of ct));
-  in bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt ct end;
+  in
+    ct
+    |> bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt
+    |> Thm.solve_constraints
+  end;
 
 val simple_prover =
   SINGLE o (fn ctxt => ALLGOALS (resolve_tac ctxt (prems_of ctxt)));
--- a/src/Pure/thm.ML	Tue Aug 06 18:04:06 2019 +0200
+++ b/src/Pure/thm.ML	Tue Aug 06 20:52:06 2019 +0200
@@ -1576,6 +1576,7 @@
           hyps = hyps,
           tpairs = tpairs',
           prop = prop'})
+        |> solve_constraints
       end
       handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);
 
@@ -2155,7 +2156,7 @@
 (*Resolution: exactly one resolvent must be produced*)
 fun tha RSN (i, thb) =
   (case Seq.chop 2 (biresolution NONE false [(false, tha)] i thb) of
-    ([th], _) => th
+    ([th], _) => solve_constraints th
   | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb])
   | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb]));
 
--- a/src/ZF/Datatype.thy	Tue Aug 06 18:04:06 2019 +0200
+++ b/src/ZF/Datatype.thy	Tue Aug 06 20:52:06 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 18:04:06 2019 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Tue Aug 06 20:52:06 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 18:04:06 2019 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Tue Aug 06 20:52:06 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 18:04:06 2019 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Tue Aug 06 20:52:06 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)
--- a/src/ZF/arith_data.ML	Tue Aug 06 18:04:06 2019 +0200
+++ b/src/ZF/arith_data.ML	Tue Aug 06 20:52:06 2019 +0200
@@ -164,8 +164,8 @@
   val prove_conv = prove_conv "nateq_cancel_numerals"
   val mk_bal   = FOLogic.mk_eq
   val dest_bal = FOLogic.dest_eq
-  val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans}
-  val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans}
+  val bal_add1 = @{thm eq_add_iff [THEN iff_trans]}
+  val bal_add2 = @{thm eq_add_iff [THEN iff_trans]}
   fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
   end;
 
@@ -177,8 +177,8 @@
   val prove_conv = prove_conv "natless_cancel_numerals"
   val mk_bal   = FOLogic.mk_binrel \<^const_name>\<open>Ordinal.lt\<close>
   val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Ordinal.lt\<close> iT
-  val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
-  val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
+  val bal_add1 = @{thm less_add_iff [THEN iff_trans]}
+  val bal_add2 = @{thm less_add_iff [THEN iff_trans]}
   fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
   end;
 
@@ -190,8 +190,8 @@
   val prove_conv = prove_conv "natdiff_cancel_numerals"
   val mk_bal   = FOLogic.mk_binop \<^const_name>\<open>Arith.diff\<close>
   val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Arith.diff\<close> iT
-  val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
-  val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
+  val bal_add1 = @{thm diff_add_eq [THEN trans]}
+  val bal_add2 = @{thm diff_add_eq [THEN trans]}
   fun trans_tac ctxt = gen_trans_tac ctxt @{thm trans}
   end;