# HG changeset patch
# User haftmann
# Date 1136284336 -3600
# Node ID 59b89f625d687d6b9a14f7fbf38f9850c5e72f1f
# Parent  5308a6ea3b96eb0a53303a9da5019a58251afd5b
add_local_context now yields imported and body elements seperatly; additional slight clenup in code

diff -r 5308a6ea3b96 -r 59b89f625d68 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Jan 03 11:31:15 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Jan 03 11:32:16 2006 +0100
@@ -63,9 +63,11 @@
   val print_local_registrations: bool -> string -> ProofContext.context -> unit
 
   val add_locale_context: bool -> bstring -> expr -> Element.context list -> theory
-    -> (Element.context_i list * ProofContext.context) * theory
+    -> ((Element.context_i list list * Element.context_i list list)
+         * ProofContext.context) * theory
   val add_locale_context_i: bool -> bstring -> expr -> Element.context_i list -> theory
-    -> (Element.context_i list * ProofContext.context) * theory
+    -> ((Element.context_i list list * Element.context_i list list)
+         * ProofContext.context) * theory
   val add_locale: bool -> bstring -> expr -> Element.context list -> theory -> theory
   val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory -> theory
 
@@ -1201,7 +1203,7 @@
        the fixes elements in raw_elemss,
        raw_proppss contains assumptions and definitions from the
        external elements in raw_elemss. *)
-    fun prep_prop raw_ctxt raw_concl raw_propp =
+    fun prep_prop raw_propp (raw_ctxt, raw_concl)  =
       let
         (* CB: add type information from fixed_params to context (declare_term) *)
         (* CB: process patterns (conclusion and external elements only) *)
@@ -1213,9 +1215,10 @@
         val all_propp' = map2 (curry (op ~~))
           (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
         val (concl, propp) = splitAt (length raw_concl, all_propp')
-      in ((ctxt, concl), propp) end
+      in (propp, (ctxt, concl)) end
 
-    val ((ctxt, concl), proppss) = (burrow_split o burrow_split) (prep_prop raw_ctxt raw_concl) raw_proppss;
+    val (proppss, (ctxt, concl)) =
+      (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
 
     (* CB: obtain all parameters from identifier part of raw_elemss *)
     val xs = map #1 (params_of' raw_elemss);
@@ -1608,21 +1611,33 @@
       prove_protected defs_thy t
        (Tactic.rewrite_goals_tac defs THEN
         Tactic.compose_tac (false, ax, 0) 1));
-  in (defs_thy, (statement, intro, axioms)) end;
+  in ((statement, intro, axioms), defs_thy) end;
 
-fun assumes_to_notes (axms, Assumes asms) =
-      apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) =>
-        let val (ps, qs) = splitAt (length spec, axs)
-        in (qs, (a, [(ps, [])])) end))
-  | assumes_to_notes e = e;
+fun assumes_to_notes (Assumes asms) axms =
+       axms
+       |> fold_map (fn (a, spec) => fn axs =>
+            let val (ps, qs) = splitAt (length spec, axs)
+            in ((a, [(ps, [])]), qs) end
+          ) asms
+       |-> (fn asms' => pair (Notes asms'))
+  | assumes_to_notes e axms = (e, axms);
 
 (* CB: changes only "new" elems, these have identifier ("", _). *)
 
-fun change_elemss axioms elemss = (map (conclude_protected o #2) axioms, elemss) |> foldl_map
-  (fn (axms, (id as ("", _), es)) =>
-    foldl_map assumes_to_notes (axms, map (Element.map_ctxt_values I I (satisfy_protected axioms)) es)
-    |> apsnd (pair id)
-  | x => x) |> #2;
+fun change_elemss axioms (import_elemss, body_elemss) =
+  let
+    fun change (id as ("", _), es)=
+          fold_map assumes_to_notes
+            (map (Element.map_ctxt_values I I (satisfy_protected axioms)) es)
+          #-> (fn es' => pair (id, es'))
+      | change e = pair e;
+  in
+    axioms
+    |> map (conclude_protected o #2)
+    |> fold_map change import_elemss
+    ||>> fold_map change body_elemss
+    |> fst
+  end;
 
 in
 
@@ -1630,26 +1645,30 @@
 
 fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
   let
-    val (thy', (elemss', more_ts)) =
-      if null exts then (thy, (elemss, []))
+    val ((elemss', more_ts), thy') =
+      if null exts then ((elemss, []), thy)
       else
         let
           val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
-          val (def_thy, (statement, intro, axioms)) =
+          val ((statement, intro, axioms), def_thy) =
             thy |> def_pred aname parms defs exts exts';
-          val elemss' = change_elemss axioms elemss @
-            [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
+          val elemss' =
+            elemss
+            |> change_elemss axioms
+            |> apsnd (fn elems => elems @ 
+                 [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])]
+               );
         in
           def_thy
           |> note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
           |> snd
-          |> rpair (elemss', [statement])
+          |> pair (elemss', [statement])
         end;
-    val (thy'', predicate) =
-      if null ints then (thy', ([], []))
+    val (predicate, thy'') =
+      if null ints then (([], []), thy')
       else
         let
-          val (def_thy, (statement, intro, axioms)) =
+          val ((statement, intro, axioms), def_thy) =
             thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
           val cstatement = Thm.cterm_of def_thy statement;
         in
@@ -1658,9 +1677,9 @@
                [((introN, []), [([intro], [])]),
                 ((axiomsN, []), [(map (Drule.standard o conclude_protected o #2) axioms, [])])]
           |> snd
-          |> rpair ([cstatement], axioms)
+          |> pair ([cstatement], axioms)
         end;
-  in (thy'', (elemss', predicate)) end;
+  in ((elemss', predicate), thy'') end;
 
 end;
 
@@ -1680,7 +1699,7 @@
     val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
       text as (parms, ((_, exts'), _), _)) =
       prep_ctxt raw_import raw_body thy_ctxt;
-    val elemss = import_elemss @ body_elemss;
+    val elemss = (import_elemss, body_elemss);
     val import = prep_expr thy raw_import;
 
     val extraTs = foldr Term.add_term_tfrees [] exts' \\
@@ -1688,9 +1707,9 @@
     val _ = if null extraTs then ()
       else warning ("Additional type variable(s) in locale specification " ^ quote bname);
 
-    val (pred_thy, (elemss', predicate as (predicate_statement, predicate_axioms))) =
+    val ((elemss', predicate as (predicate_statement, predicate_axioms)), pred_thy) =
       if do_predicate then thy |> define_preds bname text elemss
-      else (thy, (elemss, ([], [])));
+      else ((elemss, ([], [])), thy);
 
     fun axiomify axioms elemss =
       (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
@@ -1700,20 +1719,20 @@
                  in (axs2, ((id, Assumed axs1), elems)) end)
         |> snd;
     val (ctxt, (_, facts)) = activate_facts (K I)
-      (thy_ctxt, axiomify predicate_axioms elemss');
+      (thy_ctxt, axiomify predicate_axioms ((op @) elemss'));
     val export = ProofContext.export_view predicate_statement ctxt thy_ctxt;
     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
-    val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))
+    val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) ((op @) elemss')))
   in
     pred_thy
     |> note_thmss_qualified "" name facts' |> snd
     |> declare_locale name
     |> put_locale name {predicate = predicate, import = import,
         elems = map (fn e => (e, stamp ())) elems',
-        params = (params_of elemss' |>
+        params = (params_of ((op @) elemss') |>
           map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), map #1 (params_of body_elemss)),
         regs = []}
-    |> pair (elems', body_ctxt)
+    |> pair ((fn (e1, e2) => (map snd e1, map snd e2)) elemss', body_ctxt)
   end;
 
 in
diff -r 5308a6ea3b96 -r 59b89f625d68 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Tue Jan 03 11:31:15 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Jan 03 11:32:16 2006 +0100
@@ -92,6 +92,7 @@
   let
     fun extract_notes_consts thy elems =
       elems
+      |> Library.flat
       |> List.mapPartial
            (fn (Notes notes) => SOME notes
              | _ => NONE)
@@ -112,6 +113,7 @@
            | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
     fun extract_tyvar_consts thy elems =
       elems
+      |> Library.flat
       |> List.mapPartial
            (fn (Fixes consts) => SOME consts
              | _ => NONE)
@@ -138,8 +140,8 @@
   in
     thy
     |> add_locale bname raw_import raw_body
-    |-> (fn (elems : context_i list, ctxt) =>
-       tap (fn _ => map (print_ctxt ctxt) elems)
+    |-> (fn ((_, elems : context_i list list), ctxt) =>
+       tap (fn _ => (map o map) (print_ctxt ctxt) elems)
     #> tap (fn thy => extract_notes_consts thy elems)
     #> `(fn thy => Locale.intern thy bname)
     #-> (fn name_locale =>
@@ -311,7 +313,7 @@
 
 in
 
-val classK = "class_class"
+val classK = "class"
 
 val locale_val =
   (P.locale_expr --