src/Pure/sign.ML
changeset 7640 6b7daae5d316
parent 7068 d396d8b935f1
child 8290 7015d6b11b56
equal deleted inserted replaced
7639:538bd31709cb 7640:6b7daae5d316
    42   val classes: sg -> class list
    42   val classes: sg -> class list
    43   val defaultS: sg -> sort
    43   val defaultS: sg -> sort
    44   val subsort: sg -> sort * sort -> bool
    44   val subsort: sg -> sort * sort -> bool
    45   val nodup_Vars: term -> unit
    45   val nodup_Vars: term -> unit
    46   val norm_sort: sg -> sort -> sort
    46   val norm_sort: sg -> sort -> sort
    47   val nonempty_sort: sg -> sort list -> sort -> bool
       
    48   val of_sort: sg -> typ * sort -> bool
    47   val of_sort: sg -> typ * sort -> bool
       
    48   val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
       
    49   val univ_witness: sg -> (typ * sort) option
    49   val classK: string
    50   val classK: string
    50   val typeK: string
    51   val typeK: string
    51   val constK: string
    52   val constK: string
    52   val full_name: sg -> bstring -> string
    53   val full_name: sg -> bstring -> string
    53   val full_name_path: sg -> string -> bstring -> string
    54   val full_name_path: sg -> string -> bstring -> string
   254 fun is_draft (Sg ({stamps = ref name :: _, ...}, _)) = name = "" orelse ord name = ord "#";
   255 fun is_draft (Sg ({stamps = ref name :: _, ...}, _)) = name = "" orelse ord name = ord "#";
   255 
   256 
   256 
   257 
   257 (* classes and sorts *)
   258 (* classes and sorts *)
   258 
   259 
   259 val classes = #classes o Type.rep_tsig o tsig_of;
   260 val classes = Type.classes o tsig_of;
   260 
       
   261 val defaultS = Type.defaultS o tsig_of;
   261 val defaultS = Type.defaultS o tsig_of;
   262 val subsort = Type.subsort o tsig_of;
   262 val subsort = Type.subsort o tsig_of;
   263 val norm_sort = Type.norm_sort o tsig_of;
   263 val norm_sort = Type.norm_sort o tsig_of;
   264 val nonempty_sort = Type.nonempty_sort o tsig_of;
   264 val of_sort = Type.of_sort o tsig_of;
   265 
   265 val witness_sorts = Type.witness_sorts o tsig_of;
   266 fun of_sort (Sg (_, {tsig, ...})) =
   266 val univ_witness = Type.univ_witness o tsig_of;
   267   Sorts.of_sort (#classrel (Type.rep_tsig tsig)) (#arities (Type.rep_tsig tsig));
       
   268 
   267 
   269 
   268 
   270 
   269 
   271 (** signature data **)
   270 (** signature data **)
   272 
   271