src/Pure/sign.ML
changeset 29006 abe0f11cfa4e
parent 28965 1de908189869
child 29581 b3b33e0298eb
     1.1 --- a/src/Pure/sign.ML	Fri Dec 05 18:42:39 2008 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Dec 05 18:43:42 2008 +0100
     1.3 @@ -508,10 +508,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 (Name.name_of raw_b) raw_mx;
     1.8 +        val (mx_name, mx) = Syntax.const_mixfix (Binding.base_name raw_b) raw_mx;
     1.9          val b = Binding.map_base (K mx_name) raw_b;
    1.10          val c = full_name thy b;
    1.11 -        val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b;
    1.12 +        val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
    1.13          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.14            cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
    1.15          val T' = Logic.varifyT T;