src/Pure/sign.ML
changeset 30240 5b25fee0362c
parent 29606 fedb8be05f24
child 30242 aea5d7fa7ef5
     1.1 --- a/src/Pure/sign.ML	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -338,7 +338,7 @@
     1.4      fun typ_of (_, Const (_, T)) = T
     1.5        | typ_of (_, Free  (_, T)) = T
     1.6        | typ_of (_, Var (_, T)) = T
     1.7 -      | typ_of (bs, Bound i) = snd (List.nth (bs, i) handle Subscript =>
     1.8 +      | typ_of (bs, Bound i) = snd (nth bs i handle Subscript =>
     1.9            raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i]))
    1.10        | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body)
    1.11        | typ_of (bs, t $ u) =
    1.12 @@ -507,12 +507,12 @@
    1.13      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    1.14      fun prep (raw_b, raw_T, raw_mx) =
    1.15        let
    1.16 -        val (mx_name, mx) = Syntax.const_mixfix (Binding.base_name raw_b) raw_mx;
    1.17 -        val b = Binding.map_base (K mx_name) raw_b;
    1.18 +        val (mx_name, mx) = Syntax.const_mixfix (Binding.name_of raw_b) raw_mx;
    1.19 +        val b = Binding.map_name (K mx_name) raw_b;
    1.20          val c = full_name thy b;
    1.21 -        val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
    1.22 +        val c_syn = if authentic then Syntax.constN ^ c else Binding.name_of b;
    1.23          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.24 -          cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
    1.25 +          cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
    1.26          val T' = Logic.varifyT T;
    1.27        in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
    1.28      val args = map prep raw_args;
    1.29 @@ -549,7 +549,7 @@
    1.30      val pp = Syntax.pp_global thy;
    1.31      val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
    1.32      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    1.33 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
    1.34 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
    1.35      val (res, consts') = consts_of thy
    1.36        |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
    1.37    in (res, thy |> map_consts (K consts')) end;