maintain group via name space, not tags;
authorwenzelm
Sun Oct 25 19:18:59 2009 +0100 (2009-10-25)
changeset 33167f02b804305d6
parent 33166 55f250ef9e31
child 33168 853493e5d5d4
maintain group via name space, not tags;
src/Pure/General/markup.ML
src/Pure/Isar/theory_target.ML
src/Pure/more_thm.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/General/markup.ML	Sun Oct 25 19:18:25 2009 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Sun Oct 25 19:18:59 2009 +0100
     1.3 @@ -13,7 +13,6 @@
     1.4    val nameN: string
     1.5    val name: string -> T -> T
     1.6    val bindingN: string val binding: string -> T
     1.7 -  val groupN: string
     1.8    val theory_nameN: string
     1.9    val kindN: string
    1.10    val internalK: string
    1.11 @@ -151,7 +150,6 @@
    1.12  
    1.13  val (bindingN, binding) = markup_string "binding" nameN;
    1.14  
    1.15 -val groupN = "group";
    1.16  val theory_nameN = "theory_name";
    1.17  
    1.18  
     2.1 --- a/src/Pure/Isar/theory_target.ML	Sun Oct 25 19:18:25 2009 +0100
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Oct 25 19:18:59 2009 +0100
     2.3 @@ -158,8 +158,8 @@
     2.4      val global_facts = PureThy.map_facts #2 facts'
     2.5        |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy);
     2.6    in
     2.7 -    lthy |> LocalTheory.theory
     2.8 -      (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
     2.9 +    lthy
    2.10 +    |> LocalTheory.theory (PureThy.note_thmss kind global_facts #> snd)
    2.11      |> not is_locale ? LocalTheory.target (ProofContext.note_thmss kind global_facts #> snd)
    2.12      |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
    2.13      |> ProofContext.note_thmss kind local_facts
    2.14 @@ -173,7 +173,7 @@
    2.15    else if not is_class then (NoSyn, mx, NoSyn)
    2.16    else (mx, NoSyn, NoSyn);
    2.17  
    2.18 -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((b, mx), rhs) phi =
    2.19 +fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
    2.20    let
    2.21      val b' = Morphism.binding phi b;
    2.22      val rhs' = Morphism.term phi rhs;
    2.23 @@ -187,8 +187,8 @@
    2.24    in
    2.25      not (is_class andalso (similar_body orelse class_global)) ?
    2.26        (Context.mapping_result
    2.27 -        (Sign.add_abbrev PrintMode.internal tags arg)
    2.28 -        (ProofContext.add_abbrev PrintMode.internal tags arg)
    2.29 +        (Sign.add_abbrev PrintMode.internal [] arg)
    2.30 +        (ProofContext.add_abbrev PrintMode.internal [] arg)
    2.31        #-> (fn (lhs' as Const (d, _), _) =>
    2.32            similar_body ?
    2.33              (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    2.34 @@ -199,7 +199,6 @@
    2.35  
    2.36  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
    2.37    let
    2.38 -    val tags = LocalTheory.group_position_of lthy;
    2.39      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    2.40      val U = map #2 xs ---> T;
    2.41      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    2.42 @@ -215,13 +214,13 @@
    2.43                  if mx3 <> NoSyn then syntax_error c'
    2.44                  else LocalTheory.theory_result (Overloading.declare (c', U))
    2.45                    ##> Overloading.confirm b
    2.46 -            | NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3))));
    2.47 +            | NONE => LocalTheory.theory_result (Sign.declare_const [] ((b, U), mx3))));
    2.48      val (const, lthy') = lthy |> declare_const;
    2.49      val t = Term.list_comb (const, map Free xs);
    2.50    in
    2.51      lthy'
    2.52 -    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t))
    2.53 -    |> is_class ? class_target ta (Class_Target.declare target tags ((b, mx1), t))
    2.54 +    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default ((b, mx2), t))
    2.55 +    |> is_class ? class_target ta (Class_Target.declare target [] ((b, mx1), t))
    2.56      |> LocalDefs.add_def ((b, NoSyn), t)
    2.57    end;
    2.58  
    2.59 @@ -230,7 +229,6 @@
    2.60  
    2.61  fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
    2.62    let
    2.63 -    val tags = LocalTheory.group_position_of lthy;
    2.64      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    2.65      val target_ctxt = LocalTheory.target_of lthy;
    2.66  
    2.67 @@ -243,17 +241,17 @@
    2.68    in
    2.69      lthy |>
    2.70       (if is_locale then
    2.71 -        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (b, global_rhs))
    2.72 +        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal [] (b, global_rhs))
    2.73          #-> (fn (lhs, _) =>
    2.74            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    2.75 -            term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
    2.76 -            is_class ? class_target ta (Class_Target.abbrev target prmode tags ((b, mx1), t'))
    2.77 +            term_syntax ta (locale_const ta prmode ((b, mx2), lhs')) #>
    2.78 +            is_class ? class_target ta (Class_Target.abbrev target prmode [] ((b, mx1), t'))
    2.79            end)
    2.80        else
    2.81          LocalTheory.theory
    2.82 -          (Sign.add_abbrev (#1 prmode) tags (b, global_rhs) #-> (fn (lhs, _) =>
    2.83 +          (Sign.add_abbrev (#1 prmode) [] (b, global_rhs) #-> (fn (lhs, _) =>
    2.84             Sign.notation true prmode [(lhs, mx3)])))
    2.85 -    |> ProofContext.add_abbrev PrintMode.internal tags (b, t) |> snd
    2.86 +    |> ProofContext.add_abbrev PrintMode.internal [] (b, t) |> snd
    2.87      |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
    2.88    end;
    2.89  
     3.1 --- a/src/Pure/more_thm.ML	Sun Oct 25 19:18:25 2009 +0100
     3.2 +++ b/src/Pure/more_thm.ML	Sun Oct 25 19:18:59 2009 +0100
     3.3 @@ -83,9 +83,6 @@
     3.4    val has_name_hint: thm -> bool
     3.5    val get_name_hint: thm -> string
     3.6    val put_name_hint: string -> thm -> thm
     3.7 -  val get_group: thm -> string option
     3.8 -  val put_group: string -> thm -> thm
     3.9 -  val group: string -> attribute
    3.10    val axiomK: string
    3.11    val assumptionK: string
    3.12    val definitionK: string
    3.13 @@ -417,15 +414,6 @@
    3.14  fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name);
    3.15  
    3.16  
    3.17 -(* theorem groups *)
    3.18 -
    3.19 -fun get_group thm = Properties.get (Thm.get_tags thm) Markup.groupN;
    3.20 -
    3.21 -fun put_group name = if name = "" then I else Thm.map_tags (Properties.put (Markup.groupN, name));
    3.22 -
    3.23 -fun group name = rule_attribute (K (put_group name));
    3.24 -
    3.25 -
    3.26  (* theorem kinds *)
    3.27  
    3.28  val axiomK = "axiom";
     4.1 --- a/src/Pure/pure_thy.ML	Sun Oct 25 19:18:25 2009 +0100
     4.2 +++ b/src/Pure/pure_thy.ML	Sun Oct 25 19:18:59 2009 +0100
     4.3 @@ -32,8 +32,6 @@
     4.4    val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
     4.5    val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
     4.6      -> theory -> (string * thm list) list * theory
     4.7 -  val note_thmss_grouped: string -> string -> (Thm.binding * (thm list * attribute list) list) list
     4.8 -    -> theory -> (string * thm list) list * theory
     4.9    val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
    4.10    val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
    4.11    val add_defs: bool -> ((binding * term) * attribute list) list ->
    4.12 @@ -192,9 +190,7 @@
    4.13  
    4.14  (* note_thmss *)
    4.15  
    4.16 -local
    4.17 -
    4.18 -fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
    4.19 +fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
    4.20    let
    4.21      val pos = Binding.pos_of b;
    4.22      val name = Sign.full_name thy b;
    4.23 @@ -203,16 +199,9 @@
    4.24      fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
    4.25      val (thms, thy') = thy |> enter_thms
    4.26        (name_thmss true pos) (name_thms false true pos) (apsnd flat o Library.foldl_map app)
    4.27 -      (b, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts);
    4.28 +      (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
    4.29    in ((name, thms), thy') end);
    4.30  
    4.31 -in
    4.32 -
    4.33 -fun note_thmss k = gen_note_thmss (Thm.kind k);
    4.34 -fun note_thmss_grouped k g = gen_note_thmss (Thm.kind k #> Thm.group g);
    4.35 -
    4.36 -end;
    4.37 -
    4.38  
    4.39  (* store axioms as theorems *)
    4.40