# HG changeset patch
# User haftmann
# Date 1449080096 -3600
# Node ID 2f33f6cc964d6a709bf1668ad00b179bce3d12ea
# Parent  acc532690ee1961d43254a25c74150eff65c3ec2
formally correct context for export, which got screwed up in 87203a0f0041

diff -r acc532690ee1 -r 2f33f6cc964d src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Wed Dec 02 19:14:55 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML	Wed Dec 02 19:14:56 2015 +0100
@@ -88,7 +88,7 @@
     val (def_eqns, def_ctxt) = define_mixins pre_defs expr_ctxt;
     val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns;
     val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
-    val export' = Variable.export_morphism goal_ctxt def_ctxt;
+    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
   in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
 
 in