src/Pure/sign.ML
changeset 30223 24d975352879
parent 30218 cdd82ba2b4fd
child 30242 aea5d7fa7ef5
     1.1 --- a/src/Pure/sign.ML	Tue Mar 03 18:31:59 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Mar 03 18:32:01 2009 +0100
     1.3 @@ -507,10 +507,10 @@
     1.4      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
     1.5      fun prep (raw_b, raw_T, raw_mx) =
     1.6        let
     1.7 -        val (mx_name, mx) = Syntax.const_mixfix (Binding.base_name raw_b) raw_mx;
     1.8 -        val b = Binding.map_base (K mx_name) raw_b;
     1.9 +        val (mx_name, mx) = Syntax.const_mixfix (Binding.name_of raw_b) raw_mx;
    1.10 +        val b = Binding.map_name (K mx_name) raw_b;
    1.11          val c = full_name thy b;
    1.12 -        val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
    1.13 +        val c_syn = if authentic then Syntax.constN ^ c else Binding.name_of b;
    1.14          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.15            cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
    1.16          val T' = Logic.varifyT T;