# HG changeset patch # User wenzelm # Date 1256494739 -3600 # Node ID f02b804305d6caf37cfb36d5ebf261ee8dcc7c67 # Parent 55f250ef9e313022a04aeb5cb071801295320839 maintain group via name space, not tags; diff -r 55f250ef9e31 -r f02b804305d6 src/Pure/General/markup.ML --- 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"; diff -r 55f250ef9e31 -r f02b804305d6 src/Pure/Isar/theory_target.ML --- 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; diff -r 55f250ef9e31 -r f02b804305d6 src/Pure/more_thm.ML --- 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"; diff -r 55f250ef9e31 -r f02b804305d6 src/Pure/pure_thy.ML --- 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 *)