# HG changeset patch
# User ballarin
# Date 1225360665 -3600
# Node ID e2064974c11482013c4d665eb8072c9d23b3931c
# Parent  6a5d214aaa8255250189b3a03d16e29025800171
Dropped context element 'includes'.

diff -r 6a5d214aaa82 -r e2064974c114 NEWS
--- a/NEWS	Wed Oct 29 15:32:58 2008 +0100
+++ b/NEWS	Thu Oct 30 10:57:45 2008 +0100
@@ -77,6 +77,19 @@
 * Global versions of theorems stemming from classes do not carry
 a parameter prefix any longer.  INCOMPATIBILITY.
 
+* Dropped locale element "includes".  This is a major INCOMPATIBILITY.
+In existing theorem specifications replace the includes element by the
+respective context elements of the included locale, omitting those that
+are already present in the theorem specification.  Multiple assume
+elements of a locale should be replaced by a single one involving the
+locale predicate.  In the proof body, declarations (most notably
+theorems) may be regained by interpreting the respective locales in the
+proof context as required (command "interpret").
+If using "includes" in replacement of a target solely because the
+parameter types in the theorem are not as general as in the target,
+consider declaring a new locale with additional type constraints on the
+parameters (context element "constrains").
+
 * Dropped "locale (open)".  INCOMPATBILITY.
 
 * Interpretation commands no longer attempt to simplify goal.
diff -r 6a5d214aaa82 -r e2064974c114 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Oct 29 15:32:58 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Oct 30 10:57:45 2008 +0100
@@ -41,8 +41,6 @@
     Rename of expr * (string * mixfix option) option list |
     Merge of expr list
   val empty: expr
-  datatype 'a element = Elem of 'a | Expr of expr
-  val map_elem: ('a -> 'b) -> 'a element -> 'b element
 
   val intern: theory -> xstring -> string
   val intern_expr: theory -> expr -> expr
@@ -65,13 +63,13 @@
   val declarations_of: theory -> string -> declaration list * declaration list;
 
   (* Processing of locale statements *)
-  val read_context_statement: xstring option -> Element.context element list ->
+  val read_context_statement: xstring option -> Element.context list ->
     (string * string list) list list -> Proof.context ->
     string option * Proof.context * Proof.context * (term * term list) list list
-  val read_context_statement_i: string option -> Element.context element list ->
+  val read_context_statement_i: string option -> Element.context list ->
     (string * string list) list list -> Proof.context ->
     string option * Proof.context * Proof.context * (term * term list) list list
-  val cert_context_statement: string option -> Element.context_i element list ->
+  val cert_context_statement: string option -> Element.context_i list ->
     (term * term list) list list -> Proof.context ->
     string option * Proof.context * Proof.context * (term * term list) list list
   val read_expr: expr -> Element.context list -> Proof.context ->
@@ -1541,7 +1539,7 @@
           let val {params = ps, ...} = the_locale thy name
           in (map fst ps, Locale name) end);
     val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
-      prep_ctxt false fixed_params imports elems concl ctxt;
+      prep_ctxt false fixed_params imports (map Elem elems) concl ctxt;
   in (locale, locale_ctxt, elems_ctxt, concl') end;
 
 fun prep_expr prep imports body ctxt =
diff -r 6a5d214aaa82 -r e2064974c114 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Wed Oct 29 15:32:58 2008 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Thu Oct 30 10:57:45 2008 +0100
@@ -27,11 +27,11 @@
   val class_expr: token list -> string list * token list
   val locale_expr: token list -> Locale.expr * token list
   val locale_keyword: token list -> string * token list
-  val locale_element: token list -> Element.context Locale.element * token list
+  val locale_element: token list -> Element.context * token list
   val context_element: token list -> Element.context * token list
   val statement: token list -> (Attrib.binding * (string * string list) list) list * token list
   val general_statement: token list ->
-    (Element.context Locale.element list * Element.statement) * OuterLex.token list
+    (Element.context list * Element.statement) * OuterLex.token list
   val statement_keyword: token list -> string * token list
   val specification: token list ->
     (Name.binding *
@@ -120,8 +120,7 @@
 
 val locale_keyword = loc_keyword;
 
-val locale_element = P.group "locale element"
-  (loc_element >> Locale.Elem || P.$$$ "includes" |-- P.!!! locale_expr >> Locale.Expr);
+val locale_element = P.group "locale element" loc_element;
 
 val context_element = P.group "context element" loc_element;
 
diff -r 6a5d214aaa82 -r e2064974c114 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Oct 29 15:32:58 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Oct 30 10:57:45 2008 +0100
@@ -47,11 +47,11 @@
     local_theory -> (string * thm list) list * local_theory
   val theorem: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    Element.context_i Locale.element list -> Element.statement_i ->
+    Element.context_i list -> Element.statement_i ->
     bool -> local_theory -> Proof.state
   val theorem_cmd: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    Element.context Locale.element list -> Element.statement ->
+    Element.context list -> Element.statement ->
     bool -> local_theory -> Proof.state
   val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
 end;
@@ -273,8 +273,8 @@
           let val name = Name.name_of binding
           in if name = "" then string_of_int (i + 1) else name end);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
-          Locale.Elem (Element.Constrains
-            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE))));
+          Element.Constrains
+            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE)));
 
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -325,7 +325,7 @@
     val thy = ProofContext.theory_of lthy0;
 
     val (loc, ctxt, lthy) =
-      (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
+      (case (TheoryTarget.peek lthy0, false (* exists (fn Locale.Expr _ => true | _ => false) raw_elems *)) of
         ({target, is_locale = true, ...}, true) =>
           (*temporary workaround for non-modularity of in/includes*)  (* FIXME *)
           (SOME target, ProofContext.init thy, LocalTheory.restore lthy0)
@@ -334,7 +334,7 @@
     val attrib = prep_att thy;
     val atts = map attrib raw_atts;
 
-    val elems = raw_elems |> map (Locale.map_elem (Element.map_ctxt_attrib attrib));
+    val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
     val ((prems, stmt, facts), goal_ctxt) =
       prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;