# HG changeset patch
# User wenzelm
# Date 1559653889 -7200
# Node ID 9eff9e2dc177ca76adac128d5f79f59b4cd53f82
# Parent  9fced5690f4e20ba0e7a033fe5a1d0eb124afd52
proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);

diff -r 9fced5690f4e -r 9eff9e2dc177 src/HOL/Tools/Function/fun_cases.ML
--- a/src/HOL/Tools/Function/fun_cases.ML	Tue Jun 04 13:44:59 2019 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML	Tue Jun 04 15:11:29 2019 +0200
@@ -33,7 +33,7 @@
     fun mk_elim rl =
       Thm.implies_intr cprop
         (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
-      |> singleton (Variable.export (Proof_Context.augment prop ctxt) ctxt);
+      |> singleton (Proof_Context.export (Proof_Context.augment prop ctxt) ctxt);
   in
     (case get_first (try mk_elim) (flat elims) of
       SOME r => r
diff -r 9fced5690f4e -r 9eff9e2dc177 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Jun 04 13:44:59 2019 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue Jun 04 15:11:29 2019 +0200
@@ -594,7 +594,7 @@
     fun mk_elim rl =
       Thm.implies_intr cprop
         (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
-      |> singleton (Variable.export (Proof_Context.augment prop ctxt) ctxt);
+      |> singleton (Proof_Context.export (Proof_Context.augment prop ctxt) ctxt);
   in
     (case get_first (try mk_elim) elims of
       SOME r => r
@@ -661,7 +661,7 @@
   in
     infer_instantiate ctxt' inst eq
     |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite ctxt')))
-    |> singleton (Variable.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt' ctxt)
   end