# HG changeset patch
# User wenzelm
# Date 1333463252 -7200
# Node ID 1884d34e9aabba4d43cca51eb793ce06ee0c95ee
# Parent  6a641856a0e9a5069380c674c4a4aced204c9ae6
export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);

diff -r 6a641856a0e9 -r 1884d34e9aab src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 16:10:34 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 16:27:32 2012 +0200
@@ -194,7 +194,7 @@
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
 
-    val t' = Assumption.export_term lthy thy_ctxt t;
+    val t' = Assumption.export_term lthy (Local_Theory.target_of lthy) t;
     val xs = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy t' []));
     val u = fold_rev lambda xs t';
     val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;