proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);

--- a/src/Pure/Isar/expression.ML	Mon Jun 03 23:58:20 2019 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Jun 04 13:08:05 2019 +0200
@@ -549,7 +549,7 @@
       |> fix_params fixed
       |> (fold o fold) Proof_Context.augment (propss @ eq_propss);
 
-    val export = Variable.export_morphism goal_ctxt ctxt;
+    val export = Proof_Context.export_morphism goal_ctxt ctxt;
     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
     val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
     val exp_typ = Logic.type_map exp_term;

--- a/src/Pure/Isar/interpretation.ML	Mon Jun 03 23:58:20 2019 +0200
+++ b/src/Pure/Isar/interpretation.ML	Tue Jun 04 13:08:05 2019 +0200
@@ -70,7 +70,7 @@
     val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt;
     val (def_eqns, def_ctxt) =
       augment_with_defs prep_term raw_defs deps expr_ctxt;
-    val export' = Variable.export_morphism def_ctxt expr_ctxt;
+    val export' = Proof_Context.export_morphism def_ctxt expr_ctxt;
   in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end;
 
 in

--- a/src/Pure/Isar/local_defs.ML	Mon Jun 03 23:58:20 2019 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Jun 04 13:08:05 2019 +0200
@@ -262,7 +262,7 @@
           handle ERROR msg => cat_error msg "Failed to prove definitional specification";
       in
         def_thm
-        |> singleton (Variable.export def_ctxt def_ctxt0)
+        |> singleton (Proof_Context.export def_ctxt def_ctxt0)
         |> Drule.zero_var_indexes
       end;
   in (((c, T), rhs), prove) end;