# HG changeset patch
# User haftmann
# Date 1402503725 -7200
# Node ID 2a7a789ed510ab0a6b5d262db4409b91211b0ce3
# Parent  fe3f1ca1200a1018bcc2d494fd265acaffe89ac8
mixin definitions are within scope of "for"s of import expression

diff -r fe3f1ca1200a -r 2a7a789ed510 src/Tools/permanent_interpretation.ML
--- a/src/Tools/permanent_interpretation.ML	Wed Jun 11 18:22:04 2014 +0200
+++ b/src/Tools/permanent_interpretation.ML	Wed Jun 11 18:22:05 2014 +0200
@@ -33,8 +33,8 @@
     (*defining*)
     val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
       ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
-    val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs initial_ctxt;
-    val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt initial_ctxt) o snd o snd) defs;
+    val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt1;
+    val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt1) o snd o snd) defs;
     val expr_ctxt2 = Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) expr_ctxt1;
 
     (*setting up*)