# HG changeset patch
# User wenzelm
# Date 1377023378 -7200
# Node ID f7f1636ee2ba416d7d18a9a725f57106d4ecc4c4
# Parent  d81211f61a1b4e6bb07c8b8c19f23acd0b328383
proper context;

diff -r d81211f61a1b -r f7f1636ee2ba src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Tue Aug 20 17:39:08 2013 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue Aug 20 20:29:38 2013 +0200
@@ -61,7 +61,7 @@
   let
     val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
     val bundle0 = raw_bundle
-      |> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts));
+      |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
     val bundle =
       Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
       |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);