1.1 --- a/src/Pure/Isar/theory_target.ML	Thu Nov 20 14:51:40 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Nov 20 14:55:25 2008 +0100
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title:      Pure/Isar/theory_target.ML
     1.5      ID:         $Id$
     1.6 +    ID:         $Id$
     1.7      Author:     Makarius
     1.8  
     1.9  Common theory/locale/class/instantiation/overloading targets.
    1.10 @@ -192,18 +193,18 @@
    1.11    else if not is_class then (NoSyn, mx, NoSyn)
    1.12    else (mx, NoSyn, NoSyn);
    1.13  
    1.14 -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi =
    1.15 +fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((b, mx), rhs) phi =
    1.16    let
    1.17 -    val c' = Morphism.name phi c;
    1.18 +    val b' = Morphism.name phi b;
    1.19      val rhs' = Morphism.term phi rhs;
    1.20 -    val name' = Name.name_with_prefix c';
    1.21 -    val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
    1.22 -    val arg = (name', Term.close_schematic_term rhs');
    1.23 +    val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
    1.24 +    val arg = (b', Term.close_schematic_term rhs');
    1.25      val similar_body = Type.similar_types (rhs, rhs');
    1.26      (* FIXME workaround based on educated guess *)
    1.27 -    val class_global = Name.name_of c = Name.name_of c'
    1.28 -      andalso not (null (Name.prefix_of c'))
    1.29 -      andalso (fst o snd o split_last) (Name.prefix_of c') = Class.class_prefix target;
    1.30 +    val (prefix', _) = Name.dest_binding b';
    1.31 +    val class_global = Name.name_of b = Name.name_of b'
    1.32 +      andalso not (null prefix')
    1.33 +      andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
    1.34    in
    1.35      not (is_class andalso (similar_body orelse class_global)) ?
    1.36        (Context.mapping_result
    1.37 @@ -267,7 +268,7 @@
    1.38    in
    1.39      lthy |>
    1.40       (if is_locale then
    1.41 -        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (c, global_rhs))
    1.42 +        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (b, global_rhs))
    1.43          #-> (fn (lhs, _) =>
    1.44            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    1.45              term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
    1.46 @@ -275,9 +276,9 @@
    1.47            end)
    1.48        else
    1.49          LocalTheory.theory
    1.50 -          (Sign.add_abbrev (#1 prmode) tags (c, global_rhs) #-> (fn (lhs, _) =>
    1.51 +          (Sign.add_abbrev (#1 prmode) tags (b, global_rhs) #-> (fn (lhs, _) =>
    1.52             Sign.notation true prmode [(lhs, mx3)])))
    1.53 -    |> ProofContext.add_abbrev PrintMode.internal tags (c, t) |> snd
    1.54 +    |> ProofContext.add_abbrev PrintMode.internal tags (b, t) |> snd
    1.55      |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
    1.56    end;
    1.57