--- 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