# HG changeset patch
# User wenzelm
# Date 1559646485 -7200
# Node ID 6d6839a948cf7f00e01bb8dd8ad6a12f28e1eba0
# Parent  9c19e15c854814faf3bff6ec1ad125bd9ce3a2f1
proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);

diff -r 9c19e15c8548 -r 6d6839a948cf src/Pure/Isar/expression.ML
--- 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;
diff -r 9c19e15c8548 -r 6d6839a948cf src/Pure/Isar/interpretation.ML
--- 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
diff -r 9c19e15c8548 -r 6d6839a948cf src/Pure/Isar/local_defs.ML
--- 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;