equal
deleted
inserted
replaced
449 prep {strict = false, do_close = true, fixed_frees = false} |
449 prep {strict = false, do_close = true, fixed_frees = false} |
450 raw_import init_body raw_elems [] context; |
450 raw_import init_body raw_elems [] context; |
451 (* Declare parameters and imported facts *) |
451 (* Declare parameters and imported facts *) |
452 val context' = context |> |
452 val context' = context |> |
453 fix_params fixed |> |
453 fix_params fixed |> |
454 fold (Context.proof_map o Locale.activate_facts) deps; |
454 fold Locale.activate_declarations deps; |
455 val (elems', _) = context' |> |
455 val (elems', _) = context' |> |
456 ProofContext.set_stmt true |> |
456 ProofContext.set_stmt true |> |
457 fold_map activate elems; |
457 fold_map activate elems; |
458 in ((fixed, deps, elems'), (parms, ctxt')) end; |
458 in ((fixed, deps, elems'), (parms, ctxt')) end; |
459 |
459 |