src/Pure/Isar/expression.ML
changeset 47311 1addbe2a7458
parent 47287 8f06d8ac4609
child 47315 89a4bbf9790d
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Apr 03 17:48:16 2012 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Apr 03 18:22:14 2012 +0200
     1.3 @@ -21,14 +21,14 @@
     1.4    (* Declaring locales *)
     1.5    val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
     1.6      Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
     1.7 -      * Element.context_i list) * ((string * typ) list * Proof.context)
     1.8 +      * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
     1.9    val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
    1.10      Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
    1.11 -      * Element.context_i list) * ((string * typ) list * Proof.context)
    1.12 +      * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
    1.13        (*FIXME*)
    1.14    val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
    1.15      Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
    1.16 -      * Element.context_i list) * ((string * typ) list * Proof.context)
    1.17 +      * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
    1.18    val add_locale: (local_theory -> local_theory) -> binding -> binding ->
    1.19      expression_i -> Element.context_i list -> theory -> string * local_theory
    1.20    val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding ->
    1.21 @@ -458,10 +458,10 @@
    1.22      val context' = context |>
    1.23        fix_params fixed |>
    1.24        fold (Context.proof_map o Locale.activate_facts NONE) deps;
    1.25 -    val (elems', _) = context' |>
    1.26 +    val (elems', context'') = context' |>
    1.27        Proof_Context.set_stmt true |>
    1.28        fold_map activate elems;
    1.29 -  in ((fixed, deps, elems'), (parms, ctxt')) end;
    1.30 +  in ((fixed, deps, elems', context''), (parms, ctxt')) end;
    1.31  
    1.32  in
    1.33  
    1.34 @@ -735,7 +735,7 @@
    1.35      val _ = Locale.defined thy name andalso
    1.36        error ("Duplicate definition of locale " ^ quote name);
    1.37  
    1.38 -    val ((fixed, deps, body_elems), (parms, ctxt')) =
    1.39 +    val ((fixed, deps, body_elems, _), (parms, ctxt')) =
    1.40        prep_decl raw_import I raw_body (Proof_Context.init_global thy);
    1.41      val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
    1.42