src/Pure/sign.ML
changeset 79368 a2d8ecb13d3f
parent 79345 75701d767ed9
child 79394 2ff5ffd8731b
equal deleted inserted replaced
79367:fe0b52983b7b 79368:a2d8ecb13d3f
    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 full_name_pos: theory -> binding -> string * Position.T
    47   val const_monomorphic: theory -> string -> bool
    47   val const_monomorphic: theory -> string -> bool
    48   val const_typargs: theory -> string * typ -> typ list
    48   val const_typargs: theory -> string * typ -> typ list
    49   val const_instance: theory -> string * typ list -> typ
    49   val const_instance: theory -> string * typ list -> typ
    50   val mk_const: theory -> string * typ list -> term
    50   val mk_const: theory -> string * typ list -> term
    51   val class_space: theory -> Name_Space.T
    51   val class_space: theory -> Name_Space.T
   227 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));
   228 
   228 
   229 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;
   230 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;
   231 
   231 
   232 fun bind_name thy b = (full_name thy b, Binding.default_pos_of b);
   232 fun full_name_pos thy b = (full_name thy b, Binding.default_pos_of b);
   233 
   233 
   234 
   234 
   235 
   235 
   236 (** name spaces **)
   236 (** name spaces **)
   237 
   237