locale_const: in_class workaround prevents additional locale version of class consts;
authorwenzelm
Fri Oct 26 22:10:44 2007 +0200 (2007-10-26)
changeset 252129dd61cb753ae
parent 25211 aec1cbdbca71
child 25213 48a1e80f5cdb
locale_const: in_class workaround prevents additional locale version of class consts;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Fri Oct 26 22:10:43 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Oct 26 22:10:44 2007 +0200
     1.3 @@ -169,20 +169,23 @@
     1.4    else if not is_class then (NoSyn, mx, NoSyn)
     1.5    else (mx, NoSyn, NoSyn);
     1.6  
     1.7 -fun locale_const (prmode as (mode, _)) pos ((c, mx), rhs) phi =
     1.8 +fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) pos ((c, mx), rhs) phi =
     1.9    let
    1.10      val c' = Morphism.name phi c;
    1.11      val rhs' = Morphism.term phi rhs;
    1.12      val legacy_arg = (c', Term.close_schematic_term (Logic.legacy_varify rhs'));
    1.13      val arg = (c', Term.close_schematic_term rhs');
    1.14 +    (* FIXME workaround based on educated guess *)
    1.15 +    val in_class = is_class andalso c' = NameSpace.qualified (Class.class_prefix target) c;
    1.16    in
    1.17 -    Context.mapping_result
    1.18 -      (Sign.add_abbrev PrintMode.internal pos legacy_arg)
    1.19 -      (ProofContext.add_abbrev PrintMode.internal pos arg)
    1.20 -    #-> (fn (lhs' as Const (d, _), _) =>
    1.21 -        Type.similar_types (rhs, rhs') ?
    1.22 -          (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    1.23 -           Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)])))
    1.24 +    not in_class ?
    1.25 +      (Context.mapping_result
    1.26 +        (Sign.add_abbrev PrintMode.internal pos legacy_arg)
    1.27 +        (ProofContext.add_abbrev PrintMode.internal pos arg)
    1.28 +      #-> (fn (lhs' as Const (d, _), _) =>
    1.29 +          Type.similar_types (rhs, rhs') ?
    1.30 +            (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    1.31 +             Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
    1.32    end;
    1.33  
    1.34  fun declare_const (ta as Target {target, is_locale, is_class}) depends ((c, T), mx) lthy =
    1.35 @@ -195,7 +198,7 @@
    1.36      val t = Term.list_comb (const, map Free xs);
    1.37    in
    1.38      lthy'
    1.39 -    |> is_locale ? term_syntax ta (locale_const Syntax.mode_default pos ((c, mx2), t))
    1.40 +    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default pos ((c, mx2), t))
    1.41      |> is_class ? class_target ta (Class.add_logical_const target pos ((c, mx1), t))
    1.42      |> LocalDefs.add_def ((c, NoSyn), t)
    1.43    end;
    1.44 @@ -221,7 +224,7 @@
    1.45          LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal pos (c, global_rhs))
    1.46          #-> (fn (lhs, _) =>
    1.47            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    1.48 -            term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
    1.49 +            term_syntax ta (locale_const ta prmode pos ((c, mx2), lhs')) #>
    1.50              is_class ? class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), t'))
    1.51            end)
    1.52        else