19 Proof.context -> (term * term list) list list * Proof.context |
19 Proof.context -> (term * term list) list list * Proof.context |
20 |
20 |
21 (* Declaring locales *) |
21 (* Declaring locales *) |
22 val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list -> |
22 val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list -> |
23 Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list |
23 Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list |
24 * Element.context_i list) * ((string * typ) list * Proof.context) |
24 * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) |
25 val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list -> |
25 val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list -> |
26 Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list |
26 Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list |
27 * Element.context_i list) * ((string * typ) list * Proof.context) |
27 * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) |
28 (*FIXME*) |
28 (*FIXME*) |
29 val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list -> |
29 val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list -> |
30 Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list |
30 Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list |
31 * Element.context_i list) * ((string * typ) list * Proof.context) |
31 * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) |
32 val add_locale: (local_theory -> local_theory) -> binding -> binding -> |
32 val add_locale: (local_theory -> local_theory) -> binding -> binding -> |
33 expression_i -> Element.context_i list -> theory -> string * local_theory |
33 expression_i -> Element.context_i list -> theory -> string * local_theory |
34 val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding -> |
34 val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding -> |
35 expression -> Element.context list -> theory -> string * local_theory |
35 expression -> Element.context list -> theory -> string * local_theory |
36 |
36 |
456 raw_import init_body raw_elems [] context; |
456 raw_import init_body raw_elems [] context; |
457 (* Declare parameters and imported facts *) |
457 (* Declare parameters and imported facts *) |
458 val context' = context |> |
458 val context' = context |> |
459 fix_params fixed |> |
459 fix_params fixed |> |
460 fold (Context.proof_map o Locale.activate_facts NONE) deps; |
460 fold (Context.proof_map o Locale.activate_facts NONE) deps; |
461 val (elems', _) = context' |> |
461 val (elems', context'') = context' |> |
462 Proof_Context.set_stmt true |> |
462 Proof_Context.set_stmt true |> |
463 fold_map activate elems; |
463 fold_map activate elems; |
464 in ((fixed, deps, elems'), (parms, ctxt')) end; |
464 in ((fixed, deps, elems', context''), (parms, ctxt')) end; |
465 |
465 |
466 in |
466 in |
467 |
467 |
468 fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x; |
468 fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x; |
469 fun cert_read_declaration x = prep_declaration cert_read_full_context_statement Element.activate x; |
469 fun cert_read_declaration x = prep_declaration cert_read_full_context_statement Element.activate x; |
733 let |
733 let |
734 val name = Sign.full_name thy binding; |
734 val name = Sign.full_name thy binding; |
735 val _ = Locale.defined thy name andalso |
735 val _ = Locale.defined thy name andalso |
736 error ("Duplicate definition of locale " ^ quote name); |
736 error ("Duplicate definition of locale " ^ quote name); |
737 |
737 |
738 val ((fixed, deps, body_elems), (parms, ctxt')) = |
738 val ((fixed, deps, body_elems, _), (parms, ctxt')) = |
739 prep_decl raw_import I raw_body (Proof_Context.init_global thy); |
739 prep_decl raw_import I raw_body (Proof_Context.init_global thy); |
740 val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; |
740 val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; |
741 |
741 |
742 val extraTs = |
742 val extraTs = |
743 subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []); |
743 subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []); |