src/Pure/sign.ML
changeset 79345 75701d767ed9
parent 77895 655bd3b0671b
child 79368 a2d8ecb13d3f
equal deleted inserted replaced
79344:704aea7f5203 79345:75701d767ed9
    41   val inherit_naming: theory -> Proof.context -> Context.generic
    41   val inherit_naming: theory -> Proof.context -> Context.generic
    42   val full_name: theory -> binding -> string
    42   val full_name: theory -> binding -> string
    43   val full_name_path: theory -> string -> binding -> string
    43   val full_name_path: theory -> string -> binding -> string
    44   val full_bname: theory -> bstring -> string
    44   val full_bname: theory -> bstring -> string
    45   val full_bname_path: theory -> string -> bstring -> string
    45   val full_bname_path: theory -> string -> bstring -> string
       
    46   val bind_name: theory -> binding -> string * Position.T
    46   val const_monomorphic: theory -> string -> bool
    47   val const_monomorphic: theory -> string -> bool
    47   val const_typargs: theory -> string * typ -> typ list
    48   val const_typargs: theory -> string * typ -> typ list
    48   val const_instance: theory -> string * typ list -> typ
    49   val const_instance: theory -> string * typ list -> typ
    49   val mk_const: theory -> string * typ list -> term
    50   val mk_const: theory -> string * typ list -> term
    50   val class_space: theory -> Name_Space.T
    51   val class_space: theory -> Name_Space.T
   226 fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
   227 fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
   227 
   228 
   228 fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
   229 fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
   229 fun full_bname_path thy path = full_name_path thy path o Binding.name;
   230 fun full_bname_path thy path = full_name_path thy path o Binding.name;
   230 
   231 
       
   232 fun bind_name thy b = (full_name thy b, Binding.default_pos_of b);
       
   233 
   231 
   234 
   232 
   235 
   233 (** name spaces **)
   236 (** name spaces **)
   234 
   237 
   235 val class_space = Type.class_space o tsig_of;
   238 val class_space = Type.class_space o tsig_of;