avoid spurious fact index, notably in "context begin" (via Bundle.context);
authorwenzelm
Thu May 12 10:57:09 2016 +0200 (2016-05-12 ago)
changeset 630865c8e6a751adc
parent 63085 88474b9fc844
child 63087 be252979cfe5
avoid spurious fact index, notably in "context begin" (via Bundle.context);
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu May 12 10:21:59 2016 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu May 12 10:57:09 2016 +0200
     1.3 @@ -444,9 +444,10 @@
     1.4      val ((_, _, elems, concl), _) =
     1.5        prep {strict = true, do_close = false, fixed_frees = true}
     1.6          ([], []) I raw_elems raw_stmt ctxt;
     1.7 -    val (_, ctxt') = ctxt
     1.8 +    val ctxt' = ctxt
     1.9        |> Proof_Context.set_stmt true
    1.10 -      |> fold_map activate elems;
    1.11 +      |> fold_map activate elems |> #2
    1.12 +      |> Proof_Context.restore_stmt ctxt;
    1.13    in (concl, ctxt') end;
    1.14  
    1.15  in
    1.16 @@ -475,7 +476,8 @@
    1.17        |> fold (Context.proof_map o Locale.activate_facts NONE) deps;
    1.18      val (elems', ctxt'') = ctxt'
    1.19        |> Proof_Context.set_stmt true
    1.20 -      |> fold_map activate elems;
    1.21 +      |> fold_map activate elems
    1.22 +      ||> Proof_Context.restore_stmt ctxt';
    1.23    in ((fixed, deps, elems', ctxt''), (parms, ctxt0)) end;
    1.24  
    1.25  in