grouped versions of axioms/define/notes;

--- a/src/Pure/Isar/local_theory.ML	Sat Jan 26 17:08:42 2008 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sat Jan 26 17:08:43 2008 +0100
@@ -24,17 +24,29 @@
   val axioms: string ->
     ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
     -> (term list * (bstring * thm list) list) * local_theory
+  val axioms_grouped: string -> string ->
+    ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
+    -> (term list * (bstring * thm list) list) * local_theory
   val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
     (term * term) * local_theory
   val define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
     (term * (bstring * thm)) * local_theory
+  val define_grouped: string -> string ->
+    (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
+    (term * (bstring * thm)) * local_theory
+  val note: string -> (bstring * Attrib.src list) * thm list ->
+    local_theory -> (bstring * thm list) * local_theory
   val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     local_theory -> (bstring * thm list) list * local_theory
+  val note_grouped: string -> string ->
+    (bstring * Attrib.src list) * thm list ->
+    local_theory -> (bstring * thm list) * local_theory
+  val notes_grouped: string -> string ->
+    ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+    local_theory -> (bstring * thm list) list * local_theory
   val type_syntax: declaration -> local_theory -> local_theory
   val term_syntax: declaration -> local_theory -> local_theory
   val declaration: declaration -> local_theory -> local_theory
-  val note: string -> (bstring * Attrib.src list) * thm list ->
-    local_theory -> (bstring * thm list) * local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
   val init: string -> operations -> Proof.context -> local_theory
@@ -52,13 +64,14 @@
 
 type operations =
  {pretty: local_theory -> Pretty.T list,
-  axioms: string ->
+  axioms: string -> string ->
     ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
     -> (term list * (bstring * thm list) list) * local_theory,
   abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
-  define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
+  define: string -> string ->
+    (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
     (term * (bstring * thm)) * local_theory,
-  notes: string ->
+  notes: string -> string ->
     ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     local_theory -> (bstring * thm list) list * local_theory,
   type_syntax: declaration -> local_theory -> local_theory,
@@ -144,17 +157,24 @@
 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
 fun operation1 f x = operation (fn ops => f ops x);
 fun operation2 f x y = operation (fn ops => f ops x y);
+fun operation3 f x y z = operation (fn ops => f ops x y z);
 
 val pretty = operation #pretty;
-val axioms = operation2 #axioms;
+val axioms_grouped = operation3 #axioms;
 val abbrev = operation2 #abbrev;
-val define = operation2 #define;
-val notes = operation2 #notes;
+val define_grouped = operation3 #define;
+val notes_grouped = operation3 #notes;
 val type_syntax = operation1 #type_syntax;
 val term_syntax = operation1 #term_syntax;
 val declaration = operation1 #declaration;
 
-fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> the_single;
+fun note_grouped kind group (a, ths) lthy = lthy
+  |> notes_grouped kind group [(a, [(ths, [])])] |>> the_single;
+
+fun axioms kind = axioms_grouped kind "";
+fun define kind = define_grouped kind "";
+fun notes kind = notes_grouped kind "";
+fun note kind = note_grouped kind "";
 
 fun target_morphism lthy =
   ProofContext.export_morphism lthy (target_of lthy) $>

--- a/src/Pure/Isar/theory_target.ML	Sat Jan 26 17:08:42 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sat Jan 26 17:08:43 2008 +0100
@@ -150,7 +150,7 @@
   |> ProofContext.note_thmss_i kind facts
   ||> ProofContext.restore_naming ctxt;
 
-fun notes (Target {target, is_locale, ...}) kind facts lthy =
+fun notes (Target {target, is_locale, ...}) kind group facts lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val full = LocalTheory.full_name lthy;
@@ -167,7 +167,7 @@
   in
     lthy |> LocalTheory.theory
       (Sign.qualified_names
-        #> PureThy.note_thmss_i kind global_facts #> snd
+        #> PureThy.note_thmss_grouped kind group global_facts #> snd
         #> Sign.restore_naming thy)
 
     |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
@@ -265,7 +265,7 @@
 (* define *)
 
 fun define (ta as Target {target, is_locale, is_class, ...})
-    kind ((c, mx), ((name, atts), rhs)) lthy =
+    kind group ((c, mx), ((name, atts), rhs)) lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val thy_ctxt = ProofContext.init thy;
@@ -296,13 +296,13 @@
 
     (*note*)
     val ([(res_name, [res])], lthy4) = lthy3
-      |> notes ta kind [((name', atts), [([def], [])])];
+      |> notes ta kind group [((name', atts), [([def], [])])];
   in ((lhs, (res_name, res)), lthy4) end;
 
 
 (* axioms *)
 
-fun axioms ta kind (vars, specs) lthy =
+fun axioms ta kind group (vars, specs) lthy =
   let
     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
     val expanded_props = map (Assumption.export_term lthy thy_ctxt) (maps snd specs);
@@ -322,7 +322,7 @@
     |> fold Variable.declare_term expanded_props
     |> LocalTheory.theory (fold (fn c => Theory.add_deps "" c []) global_consts)
     |> LocalTheory.theory_result (fold_map axiom specs)
-    |-> notes ta kind
+    |-> notes ta kind group
     |>> pair (map #1 consts)
   end;