src/Pure/sign.ML
changeset 28965 1de908189869
parent 28941 128459bd72d2
child 29006 abe0f11cfa4e
     1.1 --- a/src/Pure/sign.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/sign.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -14,11 +14,10 @@
     1.4      tsig: Type.tsig,
     1.5      consts: Consts.T}
     1.6    val naming_of: theory -> NameSpace.naming
     1.7 +  val full_name: theory -> Binding.T -> string
     1.8    val base_name: string -> bstring
     1.9 -  val full_name: theory -> bstring -> string
    1.10 -  val full_binding: theory -> Name.binding -> string
    1.11 -  val full_name_path: theory -> string -> bstring -> string
    1.12 -  val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
    1.13 +  val full_bname: theory -> bstring -> string
    1.14 +  val full_bname_path: theory -> string -> bstring -> string
    1.15    val syn_of: theory -> Syntax.syntax
    1.16    val tsig_of: theory -> Type.tsig
    1.17    val classes_of: theory -> Sorts.algebra
    1.18 @@ -92,10 +91,10 @@
    1.19    val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
    1.20    val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
    1.21    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
    1.22 -  val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
    1.23 +  val declare_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
    1.24    val add_consts: (bstring * string * mixfix) list -> theory -> theory
    1.25    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    1.26 -  val add_abbrev: string -> Properties.T -> Name.binding * term -> theory -> (term * term) * theory
    1.27 +  val add_abbrev: string -> Properties.T -> Binding.T * term -> theory -> (term * term) * theory
    1.28    val revert_abbrev: string -> string -> theory -> theory
    1.29    val add_const_constraint: string * typ option -> theory -> theory
    1.30    val primitive_class: string * class list -> theory -> theory
    1.31 @@ -189,10 +188,10 @@
    1.32  val naming_of = #naming o rep_sg;
    1.33  val base_name = NameSpace.base;
    1.34  
    1.35 -val full_name = NameSpace.full o naming_of;
    1.36 -val full_binding = NameSpace.full_binding o naming_of;
    1.37 -fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
    1.38 -val declare_name = NameSpace.declare o naming_of;
    1.39 +val full_name = NameSpace.full_name o naming_of;
    1.40 +fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
    1.41 +fun full_bname_path thy elems =
    1.42 +  NameSpace.full_name (NameSpace.add_path elems (naming_of thy)) o Binding.name;
    1.43  
    1.44  
    1.45  (* syntax *)
    1.46 @@ -510,11 +509,11 @@
    1.47      fun prep (raw_b, raw_T, raw_mx) =
    1.48        let
    1.49          val (mx_name, mx) = Syntax.const_mixfix (Name.name_of raw_b) raw_mx;
    1.50 -        val b = Name.map_name (K mx_name) raw_b;
    1.51 -        val c = full_binding thy b;
    1.52 +        val b = Binding.map_base (K mx_name) raw_b;
    1.53 +        val c = full_name thy b;
    1.54          val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b;
    1.55          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.56 -          cat_error msg ("in declaration of constant " ^ quote (Name.display b));
    1.57 +          cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
    1.58          val T' = Logic.varifyT T;
    1.59        in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
    1.60      val args = map prep raw_args;
    1.61 @@ -526,7 +525,7 @@
    1.62      |> pair (map #3 args)
    1.63    end;
    1.64  
    1.65 -fun bindify (name, T, mx) = (Name.binding name, T, mx);
    1.66 +fun bindify (name, T, mx) = (Binding.name name, T, mx);
    1.67  
    1.68  in
    1.69  
    1.70 @@ -551,7 +550,7 @@
    1.71      val pp = Syntax.pp_global thy;
    1.72      val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
    1.73      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    1.74 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
    1.75 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
    1.76      val (res, consts') = consts_of thy
    1.77        |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
    1.78    in (res, thy |> map_consts (K consts')) end;