maintain group via name space, not tags;

--- a/src/Pure/General/markup.ML	Sun Oct 25 19:18:25 2009 +0100
+++ b/src/Pure/General/markup.ML	Sun Oct 25 19:18:59 2009 +0100
@@ -13,7 +13,6 @@
   val nameN: string
   val name: string -> T -> T
   val bindingN: string val binding: string -> T
-  val groupN: string
   val theory_nameN: string
   val kindN: string
   val internalK: string
@@ -151,7 +150,6 @@
 
 val (bindingN, binding) = markup_string "binding" nameN;
 
-val groupN = "group";
 val theory_nameN = "theory_name";
 
 

--- a/src/Pure/Isar/theory_target.ML	Sun Oct 25 19:18:25 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sun Oct 25 19:18:59 2009 +0100
@@ -158,8 +158,8 @@
     val global_facts = PureThy.map_facts #2 facts'
       |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy);
   in
-    lthy |> LocalTheory.theory
-      (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
+    lthy
+    |> LocalTheory.theory (PureThy.note_thmss kind global_facts #> snd)
     |> not is_locale ? LocalTheory.target (ProofContext.note_thmss kind global_facts #> snd)
     |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
     |> ProofContext.note_thmss kind local_facts
@@ -173,7 +173,7 @@
   else if not is_class then (NoSyn, mx, NoSyn)
   else (mx, NoSyn, NoSyn);
 
-fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((b, mx), rhs) phi =
+fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
   let
     val b' = Morphism.binding phi b;
     val rhs' = Morphism.term phi rhs;
@@ -187,8 +187,8 @@
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
-        (Sign.add_abbrev PrintMode.internal tags arg)
-        (ProofContext.add_abbrev PrintMode.internal tags arg)
+        (Sign.add_abbrev PrintMode.internal [] arg)
+        (ProofContext.add_abbrev PrintMode.internal [] arg)
       #-> (fn (lhs' as Const (d, _), _) =>
           similar_body ?
             (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
@@ -199,7 +199,6 @@
 
 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   let
-    val tags = LocalTheory.group_position_of lthy;
     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
     val U = map #2 xs ---> T;
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
@@ -215,13 +214,13 @@
                 if mx3 <> NoSyn then syntax_error c'
                 else LocalTheory.theory_result (Overloading.declare (c', U))
                   ##> Overloading.confirm b
-            | NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3))));
+            | NONE => LocalTheory.theory_result (Sign.declare_const [] ((b, U), mx3))));
     val (const, lthy') = lthy |> declare_const;
     val t = Term.list_comb (const, map Free xs);
   in
     lthy'
-    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t))
-    |> is_class ? class_target ta (Class_Target.declare target tags ((b, mx1), t))
+    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default ((b, mx2), t))
+    |> is_class ? class_target ta (Class_Target.declare target [] ((b, mx1), t))
     |> LocalDefs.add_def ((b, NoSyn), t)
   end;
 
@@ -230,7 +229,6 @@
 
 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   let
-    val tags = LocalTheory.group_position_of lthy;
     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
     val target_ctxt = LocalTheory.target_of lthy;
 
@@ -243,17 +241,17 @@
   in
     lthy |>
      (if is_locale then
-        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (b, global_rhs))
+        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal [] (b, global_rhs))
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
-            term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
-            is_class ? class_target ta (Class_Target.abbrev target prmode tags ((b, mx1), t'))
+            term_syntax ta (locale_const ta prmode ((b, mx2), lhs')) #>
+            is_class ? class_target ta (Class_Target.abbrev target prmode [] ((b, mx1), t'))
           end)
       else
         LocalTheory.theory
-          (Sign.add_abbrev (#1 prmode) tags (b, global_rhs) #-> (fn (lhs, _) =>
+          (Sign.add_abbrev (#1 prmode) [] (b, global_rhs) #-> (fn (lhs, _) =>
            Sign.notation true prmode [(lhs, mx3)])))
-    |> ProofContext.add_abbrev PrintMode.internal tags (b, t) |> snd
+    |> ProofContext.add_abbrev PrintMode.internal [] (b, t) |> snd
     |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
   end;
 

--- a/src/Pure/more_thm.ML	Sun Oct 25 19:18:25 2009 +0100
+++ b/src/Pure/more_thm.ML	Sun Oct 25 19:18:59 2009 +0100
@@ -83,9 +83,6 @@
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
-  val get_group: thm -> string option
-  val put_group: string -> thm -> thm
-  val group: string -> attribute
   val axiomK: string
   val assumptionK: string
   val definitionK: string
@@ -417,15 +414,6 @@
 fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name);
 
 
-(* theorem groups *)
-
-fun get_group thm = Properties.get (Thm.get_tags thm) Markup.groupN;
-
-fun put_group name = if name = "" then I else Thm.map_tags (Properties.put (Markup.groupN, name));
-
-fun group name = rule_attribute (K (put_group name));
-
-
 (* theorem kinds *)
 
 val axiomK = "axiom";

--- a/src/Pure/pure_thy.ML	Sun Oct 25 19:18:25 2009 +0100
+++ b/src/Pure/pure_thy.ML	Sun Oct 25 19:18:59 2009 +0100
@@ -32,8 +32,6 @@
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
     -> theory -> (string * thm list) list * theory
-  val note_thmss_grouped: string -> string -> (Thm.binding * (thm list * attribute list) list) list
-    -> theory -> (string * thm list) list * theory
   val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
   val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
   val add_defs: bool -> ((binding * term) * attribute list) list ->
@@ -192,9 +190,7 @@
 
 (* note_thmss *)
 
-local
-
-fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
+fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
   let
     val pos = Binding.pos_of b;
     val name = Sign.full_name thy b;
@@ -203,16 +199,9 @@
     fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
     val (thms, thy') = thy |> enter_thms
       (name_thmss true pos) (name_thms false true pos) (apsnd flat o Library.foldl_map app)
-      (b, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts);
+      (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
   in ((name, thms), thy') end);
 
-in
-
-fun note_thmss k = gen_note_thmss (Thm.kind k);
-fun note_thmss_grouped k g = gen_note_thmss (Thm.kind k #> Thm.group g);
-
-end;
-
 
 (* store axioms as theorems *)