src/Pure/Isar/theory_target.ML
changeset 33167 f02b804305d6
parent 32785 ec5292653aff
child 33173 b8ca12f6681a
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sun Oct 25 19:18:25 2009 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Oct 25 19:18:59 2009 +0100
     1.3 @@ -158,8 +158,8 @@
     1.4      val global_facts = PureThy.map_facts #2 facts'
     1.5        |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy);
     1.6    in
     1.7 -    lthy |> LocalTheory.theory
     1.8 -      (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
     1.9 +    lthy
    1.10 +    |> LocalTheory.theory (PureThy.note_thmss kind global_facts #> snd)
    1.11      |> not is_locale ? LocalTheory.target (ProofContext.note_thmss kind global_facts #> snd)
    1.12      |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
    1.13      |> ProofContext.note_thmss kind local_facts
    1.14 @@ -173,7 +173,7 @@
    1.15    else if not is_class then (NoSyn, mx, NoSyn)
    1.16    else (mx, NoSyn, NoSyn);
    1.17  
    1.18 -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((b, mx), rhs) phi =
    1.19 +fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
    1.20    let
    1.21      val b' = Morphism.binding phi b;
    1.22      val rhs' = Morphism.term phi rhs;
    1.23 @@ -187,8 +187,8 @@
    1.24    in
    1.25      not (is_class andalso (similar_body orelse class_global)) ?
    1.26        (Context.mapping_result
    1.27 -        (Sign.add_abbrev PrintMode.internal tags arg)
    1.28 -        (ProofContext.add_abbrev PrintMode.internal tags arg)
    1.29 +        (Sign.add_abbrev PrintMode.internal [] arg)
    1.30 +        (ProofContext.add_abbrev PrintMode.internal [] arg)
    1.31        #-> (fn (lhs' as Const (d, _), _) =>
    1.32            similar_body ?
    1.33              (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    1.34 @@ -199,7 +199,6 @@
    1.35  
    1.36  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
    1.37    let
    1.38 -    val tags = LocalTheory.group_position_of lthy;
    1.39      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.40      val U = map #2 xs ---> T;
    1.41      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.42 @@ -215,13 +214,13 @@
    1.43                  if mx3 <> NoSyn then syntax_error c'
    1.44                  else LocalTheory.theory_result (Overloading.declare (c', U))
    1.45                    ##> Overloading.confirm b
    1.46 -            | NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3))));
    1.47 +            | NONE => LocalTheory.theory_result (Sign.declare_const [] ((b, U), mx3))));
    1.48      val (const, lthy') = lthy |> declare_const;
    1.49      val t = Term.list_comb (const, map Free xs);
    1.50    in
    1.51      lthy'
    1.52 -    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t))
    1.53 -    |> is_class ? class_target ta (Class_Target.declare target tags ((b, mx1), t))
    1.54 +    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default ((b, mx2), t))
    1.55 +    |> is_class ? class_target ta (Class_Target.declare target [] ((b, mx1), t))
    1.56      |> LocalDefs.add_def ((b, NoSyn), t)
    1.57    end;
    1.58  
    1.59 @@ -230,7 +229,6 @@
    1.60  
    1.61  fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
    1.62    let
    1.63 -    val tags = LocalTheory.group_position_of lthy;
    1.64      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    1.65      val target_ctxt = LocalTheory.target_of lthy;
    1.66  
    1.67 @@ -243,17 +241,17 @@
    1.68    in
    1.69      lthy |>
    1.70       (if is_locale then
    1.71 -        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (b, global_rhs))
    1.72 +        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal [] (b, global_rhs))
    1.73          #-> (fn (lhs, _) =>
    1.74            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    1.75 -            term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
    1.76 -            is_class ? class_target ta (Class_Target.abbrev target prmode tags ((b, mx1), t'))
    1.77 +            term_syntax ta (locale_const ta prmode ((b, mx2), lhs')) #>
    1.78 +            is_class ? class_target ta (Class_Target.abbrev target prmode [] ((b, mx1), t'))
    1.79            end)
    1.80        else
    1.81          LocalTheory.theory
    1.82 -          (Sign.add_abbrev (#1 prmode) tags (b, global_rhs) #-> (fn (lhs, _) =>
    1.83 +          (Sign.add_abbrev (#1 prmode) [] (b, global_rhs) #-> (fn (lhs, _) =>
    1.84             Sign.notation true prmode [(lhs, mx3)])))
    1.85 -    |> ProofContext.add_abbrev PrintMode.internal tags (b, t) |> snd
    1.86 +    |> ProofContext.add_abbrev PrintMode.internal [] (b, t) |> snd
    1.87      |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
    1.88    end;
    1.89