export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);

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