abbrevs: mode does not affect name space;
authorwenzelm
Sun Apr 09 18:51:19 2006 +0200 (2006-04-09)
changeset 19384c5ee8f756683
parent 19383 a7c055012a8c
child 19385 c0f2f8224ea8
abbrevs: mode does not affect name space;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Sun Apr 09 18:51:17 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Apr 09 18:51:19 2006 +0200
     1.3 @@ -766,19 +766,17 @@
     1.4  
     1.5  fun gen_abbrevs prep_term (mode, inout) = fold (fn (raw_c, raw_t, raw_mx) => fn thy =>
     1.6    let
     1.7 -    val naming = naming_of thy
     1.8 -      |> K (mode <> "") ? (NameSpace.add_path mode #> NameSpace.no_base_names);
     1.9      val prep_tm =
    1.10        Compress.term thy o Logic.varify o no_vars (pp thy) o Term.no_dummy_patterns o prep_term thy;
    1.11  
    1.12      val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    1.13 -    val (c', b) = Syntax.mixfix_const (NameSpace.full naming c) mx;
    1.14 +    val (c', b) = Syntax.mixfix_const (full_name thy c) mx;
    1.15      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg)
    1.16        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    1.17      val T = Term.fastype_of t;
    1.18    in
    1.19      thy
    1.20 -    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) naming mode ((c, t), b))
    1.21 +    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), b))
    1.22      |> map_syn (Syntax.extend_consts [c])
    1.23      |> add_modesyntax_i (mode, inout) [(c', T, mx)]
    1.24    end);