proper context;
authorwenzelm
Tue, 20 Aug 2013 20:29:38 +0200
changeset 54248f7f1636ee2ba
parent 54243 d81211f61a1b
child 54249 04d8af9ff64b
proper context;
src/Pure/Isar/bundle.ML
     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);