src/Pure/sign.ML
changeset 19642 ea7162f84677
parent 19513 77ff7cd602d7
child 19658 0cff73279f34
equal deleted inserted replaced
19641:f1de44e61ec1 19642:ea7162f84677
    92   val full_name: theory -> bstring -> string
    92   val full_name: theory -> bstring -> string
    93   val full_name_path: theory -> string -> bstring -> string
    93   val full_name_path: theory -> string -> bstring -> string
    94   val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
    94   val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
    95   val syn_of: theory -> Syntax.syntax
    95   val syn_of: theory -> Syntax.syntax
    96   val tsig_of: theory -> Type.tsig
    96   val tsig_of: theory -> Type.tsig
    97   val classes_of: theory -> Sorts.classes
    97   val classes_of: theory -> Sorts.algebra
    98   val arities_of: theory -> Sorts.arities
       
    99   val classes: theory -> class list
    98   val classes: theory -> class list
   100   val super_classes: theory -> class -> class list
    99   val super_classes: theory -> class -> class list
   101   val defaultS: theory -> sort
   100   val defaultS: theory -> sort
   102   val subsort: theory -> sort * sort -> bool
   101   val subsort: theory -> sort * sort -> bool
   103   val of_sort: theory -> typ * sort -> bool
   102   val of_sort: theory -> typ * sort -> bool
   265 
   264 
   266 
   265 
   267 (* type signature *)
   266 (* type signature *)
   268 
   267 
   269 val tsig_of = #tsig o rep_sg;
   268 val tsig_of = #tsig o rep_sg;
   270 val classes_of = snd o #classes o Type.rep_tsig o tsig_of;
   269 val classes_of = #2 o #classes o Type.rep_tsig o tsig_of;
   271 val arities_of = #arities o Type.rep_tsig o tsig_of;
   270 val classes = Sorts.classes o classes_of;
   272 val classes = Type.classes o tsig_of;
   271 val super_classes = Sorts.super_classes o classes_of;
   273 val super_classes = Graph.imm_succs o classes_of;
       
   274 val defaultS = Type.defaultS o tsig_of;
   272 val defaultS = Type.defaultS o tsig_of;
   275 val subsort = Type.subsort o tsig_of;
   273 val subsort = Type.subsort o tsig_of;
   276 val of_sort = Type.of_sort o tsig_of;
   274 val of_sort = Type.of_sort o tsig_of;
   277 val witness_sorts = Type.witness_sorts o tsig_of;
   275 val witness_sorts = Type.witness_sorts o tsig_of;
   278 val universal_witness = Type.universal_witness o tsig_of;
   276 val universal_witness = Type.universal_witness o tsig_of;