Disallowed "includes" in locale declarations.

--- a/NEWS	Tue Aug 10 19:10:39 2004 +0200
+++ b/NEWS	Thu Aug 12 10:01:09 2004 +0200
@@ -126,6 +126,12 @@
   both Output.output and Output.raw have no effect.
 
 
+*** Isar ***
+
+* Locales:
+  - "includes" disallowed in declaration of named locales (command "locale").
+
+ 
 *** HOL ***
 
 * HOL/record: reimplementation of records. Improved scalability for

--- a/src/Pure/Isar/isar_cmd.ML	Tue Aug 10 19:10:39 2004 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 12 10:01:09 2004 +0200
@@ -215,7 +215,7 @@
 
 fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let val thy = Toplevel.theory_of state in
-    Locale.print_locale thy import (map (Locale.attribute (Attrib.local_attribute thy)) body)
+    Locale.print_locale thy import (map (Locale.map_attrib_elem (Attrib.local_attribute thy)) body)
   end);
 
 val print_attributes = Toplevel.unknown_theory o

--- a/src/Pure/Isar/isar_syn.ML	Tue Aug 10 19:10:39 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 12 10:01:09 2004 +0200
@@ -317,7 +317,7 @@
 
 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
 val general_statement =
-  statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
+  statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
 
 fun gen_theorem k =
   OuterSyntax.command k ("state " ^ k) K.thy_goal

--- a/src/Pure/Isar/isar_thy.ML	Tue Aug 10 19:10:39 2004 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Aug 12 10:01:09 2004 +0200
@@ -59,23 +59,23 @@
   val theorem_i: string -> (bstring * theory attribute list) *
     (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
   val multi_theorem: string -> bstring * Args.src list
-    -> Args.src Locale.element list
+    -> Args.src Locale.elem_or_expr list
     -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
     -> bool -> theory -> ProofHistory.T
   val multi_theorem_i: string -> bstring * theory attribute list
-    -> Proof.context attribute Locale.element_i list
+    -> Proof.context attribute Locale.elem_or_expr_i list
     -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
     -> bool -> theory -> ProofHistory.T
   val locale_multi_theorem: string -> xstring
-    -> bstring * Args.src list -> Args.src Locale.element list
+    -> bstring * Args.src list -> Args.src Locale.elem_or_expr list
     -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
     -> bool -> theory -> ProofHistory.T
   val locale_multi_theorem_i: string -> string -> bstring * Proof.context attribute list
-    -> Proof.context attribute Locale.element_i list
+    -> Proof.context attribute Locale.elem_or_expr_i list
     -> ((bstring * Proof.context attribute list) * (term * (term list * term list)) list) list
     -> bool -> theory -> ProofHistory.T
   val smart_multi_theorem: string -> xstring Library.option
-    -> bstring * Args.src list -> Args.src Locale.element list
+    -> bstring * Args.src list -> Args.src Locale.elem_or_expr list
     -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
     -> bool -> theory -> ProofHistory.T
   val assume: ((string * Args.src list) * (string * (string list * string list)) list) list
@@ -372,7 +372,7 @@
 
 fun multi_theorem k a elems concl int thy =
   global_statement (Proof.multi_theorem k None (apsnd (map (Attrib.global_attribute thy)) a)
-    (map (Locale.attribute (Attrib.local_attribute thy)) elems)) concl int thy;
+    (map (Locale.map_attrib_elem_expr (Attrib.local_attribute thy)) elems)) concl int thy;
 
 fun multi_theorem_i k a = global_statement_i o Proof.multi_theorem_i k None a;
 
@@ -380,7 +380,7 @@
   global_statement (Proof.multi_theorem k
       (Some (locale, (map (Attrib.local_attribute thy) atts,
           map (map (Attrib.local_attribute thy) o snd o fst) concl)))
-      (name, []) (map (Locale.attribute (Attrib.local_attribute thy)) elems))
+      (name, []) (map (Locale.map_attrib_elem_expr (Attrib.local_attribute thy)) elems))
       (map (apfst (apsnd (K []))) concl) int thy;
 
 fun locale_multi_theorem_i k locale (name, atts) elems concl =
@@ -578,7 +578,7 @@
 
 fun add_locale (do_pred, name, import, body) thy =
   Locale.add_locale do_pred name import
-    (map (Locale.attribute (Attrib.local_attribute thy)) body) thy;
+    (map (Locale.map_attrib_elem (Attrib.local_attribute thy)) body) thy;
 
 
 (* theory init and exit *)

--- a/src/Pure/Isar/locale.ML	Tue Aug 10 19:10:39 2004 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 12 10:01:09 2004 +0200
@@ -35,16 +35,20 @@
     Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr
   type 'att element
   type 'att element_i
+  type 'att elem_or_expr
+  type 'att elem_or_expr_i
   type locale
   val intern: Sign.sg -> xstring -> string
   val cond_extern: Sign.sg -> string -> xstring
   val the_locale: theory -> string -> locale
-  val attribute: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem_expr
+  val map_attrib_elem: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem
+    -> ('typ, 'term, 'thm, context attribute) elem
+  val map_attrib_elem_expr: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem_expr
     -> ('typ, 'term, 'thm, context attribute) elem_expr
-  val read_context_statement: xstring option -> context attribute element list ->
+  val read_context_statement: xstring option -> context attribute elem_or_expr list ->
     (string * (string list * string list)) list list -> context ->
     string option * cterm list * context * context * (term * (term list * term list)) list list
-  val cert_context_statement: string option -> context attribute element_i list ->
+  val cert_context_statement: string option -> context attribute elem_or_expr_i list ->
     (term * (term list * term list)) list list -> context ->
     string option * cterm list * context * context * (term * (term list * term list)) list list
   val print_locales: theory -> unit
@@ -92,8 +96,10 @@
 datatype ('typ, 'term, 'fact, 'att) elem_expr =
   Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr;
 
-type 'att element = (string, string, string, 'att) elem_expr;
-type 'att element_i = (typ, term, thm list, 'att) elem_expr;
+type 'att element = (string, string, string, 'att) elem;
+type 'att element_i = (typ, term, thm list, 'att) elem;
+type 'att elem_or_expr = (string, string, string, 'att) elem_expr;
+type 'att elem_or_expr_i = (typ, term, thm list, 'att) elem_expr;
 
 type locale =
  {view: cterm list * thm list,
@@ -116,10 +122,8 @@
      *)
   import: expr,                                                         (*dynamic import*)
   elems: ((typ, term, thm list, context attribute) elem * stamp) list,  (*static content*)
-  params: (string * typ option) list * string list};                  (*all/local params*)
-
-fun make_locale view import elems params =
- {view = view, import = import, elems = elems, params = params}: locale;
+  params: (string * typ option) list * string list,                     (*all/local params*)
+  typing: (string * typ) list};                                         (*inferred parameter types, currently unused*)
 
 
 (** theory data **)
@@ -134,8 +138,9 @@
   val prep_ext = I;
 
   (*joining of locale elements: only facts may be added later!*)
-  fun join ({view, import, elems, params}: locale, {elems = elems', ...}: locale) =
-    Some (make_locale view import (gen_merge_lists eq_snd elems elems') params);
+  fun join ({view, import, elems, params, typing}: locale, {elems = elems', ...}: locale) =
+    Some {view = view, import = import, elems = gen_merge_lists eq_snd elems elems',
+      params = params, typing = typing};
   fun merge ((space1, locs1), (space2, locs2)) =
     (NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2));
 
@@ -704,12 +709,14 @@
    * Locale expression: no effect. *)
 
 
-fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes)
-  | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms))
-  | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs))
-  | attribute attrib (Elem (Notes facts)) =
-      Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts))
-  | attribute _ (Expr expr) = Expr expr;
+fun map_attrib_elem _ (Fixes fixes) = Fixes fixes
+  | map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms)
+  | map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs)
+  | map_attrib_elem attrib (Notes facts) =
+      Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)
+
+fun map_attrib_elem_expr attrib (Elem elem) = Elem (map_attrib_elem attrib elem)
+  | map_attrib_elem_expr _ (Expr expr) = Expr expr;
 
 end;
 
@@ -894,8 +901,12 @@
 
 end;
 
+(* CB: type inference and consistency checks for locales *)
+
 fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
   let
+    (* CB: contexts computed in the course of this function are discarded.
+       They are used for type inference and consistency checks only. *)
     (* CB: raw_elemss are list of pairs consisting of identifiers and
        context elements, the latter marked as internal or external. *)
     val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
@@ -1032,10 +1043,13 @@
 
 in
 
-(* CB: arguments are: x->import, y->body (elements), z->context *)
-fun read_context x y z = #1 (gen_context true [] [] x y [] z);
-fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z);
+(* CB: processing of locales for add_locale(_i) and print_locale *)
+  (* CB: arguments are: x->import, y->body (elements), z->context *)
+fun read_context x y z = #1 (gen_context true [] [] x (map Elem y) [] z);
+fun cert_context x y z = #1 (gen_context_i true [] [] x (map Elem y) [] z);
 
+(* CB: processing of locales for note_thmss(_i),
+   Proof.multi_theorem(_i) and antiquotations with option "locale" *)
 val read_context_statement = gen_statement intern gen_context;
 val cert_context_statement = gen_statement (K I) gen_context_i;
 
@@ -1280,10 +1294,11 @@
 
 fun put_facts loc args thy =
   let
-    val {view, import, elems, params} = the_locale thy loc;
+    val {view, import, elems, params, typing} = the_locale thy loc;
     val note = Notes (map (fn ((a, more_atts), th_atts) =>
       ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args);
-  in thy |> put_locale loc (make_locale view import (elems @ [(note, stamp ())]) params) end;
+  in thy |> put_locale loc {view = view, import = import, elems = elems @ [(note, stamp ())],
+    params = params, typing = typing} end;
 
 fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy =
   let
@@ -1463,6 +1478,8 @@
     val thy_ctxt = ProofContext.init thy;
     val (((import_ctxt, import_elemss), (body_ctxt, body_elemss)), text) =
       prep_ctxt raw_import raw_body thy_ctxt;
+    (* typing: all parameters with their types *)
+    val (typing, _, _) = text;
     val elemss = import_elemss @ body_elemss;
 
     val (pred_thy, (elemss', view as (view_statement, view_axioms))) =
@@ -1477,9 +1494,9 @@
     pred_thy
     |> note_thmss_qualified "" name facts' |> #1
     |> declare_locale name
-    |> put_locale name (make_locale view (prep_expr sign raw_import)
-        (map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss'))))
-        (params_of elemss', map #1 (params_of body_elemss)))
+    |> put_locale name {view = view, import = prep_expr sign raw_import,
+        elems = map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss'))),
+        params = (params_of elemss', map #1 (params_of body_elemss)), typing = typing}
   end;
 
 in
@@ -1496,7 +1513,7 @@
 
 val setup =
  [LocalesData.init,
-  add_locale_i true "var" empty [Elem (Fixes [(Syntax.internal "x", None, Some Syntax.NoSyn)])],
-  add_locale_i true "struct" empty [Elem (Fixes [(Syntax.internal "S", None, None)])]];
+  add_locale_i true "var" empty [Fixes [(Syntax.internal "x", None, Some Syntax.NoSyn)]],
+  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", None, None)]]];
 
 end;

--- a/src/Pure/Isar/outer_parse.ML	Tue Aug 10 19:10:39 2004 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Thu Aug 12 10:01:09 2004 +0200
@@ -73,6 +73,7 @@
   val locale_expr: token list -> Locale.expr * token list
   val locale_keyword: token list -> string * token list
   val locale_element: token list -> Args.src Locale.element * token list
+  val locale_elem_or_expr: token list -> Args.src Locale.elem_or_expr * token list
   val method: token list -> Method.text * token list
 end;
 
@@ -305,6 +306,16 @@
 val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K None || opt_mixfix >> Some;
 val loc_keyword = $$$ "fixes" || $$$ "assumes" || $$$ "defines" || $$$ "notes" || $$$ "includes";
 
+val loc_element =
+  $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
+    >> triple1)) >> Locale.Fixes ||
+  $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
+    >> Locale.Assumes ||
+  $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
+    >> Locale.Defines ||
+  $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
+    >> Locale.Notes;
+
 fun plus1 scan =
   scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::;
 
@@ -318,15 +329,10 @@
 val locale_expr = expr0;
 val locale_keyword = loc_keyword;
 
-val locale_element = group "locale element"
-  ($$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
-    >> triple1)) >> (Locale.Elem o Locale.Fixes) ||
-  $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
-    >> (Locale.Elem o Locale.Assumes) ||
-  $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
-    >> (Locale.Elem o Locale.Defines) ||
-  $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
-    >> (Locale.Elem o Locale.Notes) ||
+val locale_element = group "locale element" loc_element;
+
+val locale_elem_or_expr = group "locale element or includes"
+  (loc_element >> Locale.Elem ||
   $$$ "includes" |-- !!! locale_expr >> Locale.Expr);
 
 end;

--- a/src/Pure/Isar/proof.ML	Tue Aug 10 19:10:39 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Aug 12 10:01:09 2004 +0200
@@ -88,13 +88,13 @@
   val invoke_case: string * string option list * context attribute list -> state -> state
   val multi_theorem: string
     -> (xstring * (context attribute list * context attribute list list)) option
-    -> bstring * theory attribute list -> context attribute Locale.element list
+    -> bstring * theory attribute list -> context attribute Locale.elem_or_expr list
     -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
     -> theory -> state
   val multi_theorem_i: string
     -> (string * (context attribute list * context attribute list list)) option
     -> bstring * theory attribute list
-    -> context attribute Locale.element_i list
+    -> context attribute Locale.elem_or_expr_i list
     -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
     -> theory -> state
   val chain: state -> state