1.1 --- a/src/Pure/Isar/bundle.ML Tue Aug 20 17:39:08 2013 +0200
1.2 +++ b/src/Pure/Isar/bundle.ML Tue Aug 20 20:29:38 2013 +0200
1.3 @@ -61,7 +61,7 @@
1.4 let
1.5 val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
1.6 val bundle0 = raw_bundle
1.7 - |> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts));
1.8 + |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
1.9 val bundle =
1.10 Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
1.11 |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);