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