tuned;
authorwenzelm
Thu May 12 10:21:59 2016 +0200 (2016-05-12 ago)
changeset 6308588474b9fc844
parent 63084 0054992a86b7
child 63086 5c8e6a751adc
tuned;
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu May 12 10:16:52 2016 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu May 12 10:21:59 2016 +0200
     1.3 @@ -464,19 +464,19 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun prep_declaration prep activate raw_import init_body raw_elems context =
     1.8 +fun prep_declaration prep activate raw_import init_body raw_elems ctxt =
     1.9    let
    1.10 -    val ((fixed, deps, elems, _), (parms, ctxt')) =
    1.11 +    val ((fixed, deps, elems, _), (parms, ctxt0)) =
    1.12        prep {strict = false, do_close = true, fixed_frees = false}
    1.13 -        raw_import init_body raw_elems (Element.Shows []) context;
    1.14 +        raw_import init_body raw_elems (Element.Shows []) ctxt;
    1.15      (* Declare parameters and imported facts *)
    1.16 -    val context' = context |>
    1.17 -      fix_params fixed |>
    1.18 -      fold (Context.proof_map o Locale.activate_facts NONE) deps;
    1.19 -    val (elems', context'') = context' |>
    1.20 -      Proof_Context.set_stmt true |>
    1.21 -      fold_map activate elems;
    1.22 -  in ((fixed, deps, elems', context''), (parms, ctxt')) end;
    1.23 +    val ctxt' = ctxt
    1.24 +      |> fix_params fixed
    1.25 +      |> fold (Context.proof_map o Locale.activate_facts NONE) deps;
    1.26 +    val (elems', ctxt'') = ctxt'
    1.27 +      |> Proof_Context.set_stmt true
    1.28 +      |> fold_map activate elems;
    1.29 +  in ((fixed, deps, elems', ctxt''), (parms, ctxt0)) end;
    1.30  
    1.31  in
    1.32