src/Pure/sign.ML
changeset 19673 853f5a3cc06e
parent 19658 0cff73279f34
child 19679 ae4c1e2742c1
     1.1 --- a/src/Pure/sign.ML	Wed May 17 01:23:44 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed May 17 01:23:46 2006 +0200
     1.3 @@ -725,7 +725,7 @@
     1.4      fun prep (raw_c, raw_T, raw_mx) =
     1.5        let
     1.6          val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
     1.7 -        val (c', b) = if early then (c, true) else Syntax.mixfix_const (full_name thy c) mx;
     1.8 +        val (c', b) = if early then (c, true) else (Syntax.constN ^ full_name thy c, false);
     1.9          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.10            cat_error msg ("in declaration of constant " ^ quote c);
    1.11        in (((c, T), b), (c', T, mx)) end;
    1.12 @@ -754,13 +754,13 @@
    1.13        Term.no_dummy_patterns o cert_term_abbrev thy;
    1.14  
    1.15      val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    1.16 -    val (c', b) = Syntax.mixfix_const (full_name thy c) mx;
    1.17 +    val c' = Syntax.constN ^ full_name thy c;
    1.18      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg)
    1.19        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    1.20      val T = Term.fastype_of t;
    1.21    in
    1.22      thy
    1.23 -    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), b))
    1.24 +    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), false))
    1.25      |> map_syn (Syntax.extend_consts [c])
    1.26      |> add_modesyntax_i (mode, inout) [(c', T, mx)]
    1.27    end);