src/Pure/defs.ML
changeset 19713 69c71d40f8a8
parent 19712 3ae3cc4b1eac
child 19727 f5895f998402
equal deleted inserted replaced
19712:3ae3cc4b1eac 19713:69c71d40f8a8
    69 
    69 
    70 datatype T = Defs of def Symtab.table;
    70 datatype T = Defs of def Symtab.table;
    71 
    71 
    72 fun lookup_list which defs c =
    72 fun lookup_list which defs c =
    73   (case Symtab.lookup defs c of
    73   (case Symtab.lookup defs c of
    74     SOME def => which def
    74     SOME (def: def) => which def
    75   | NONE => []);
    75   | NONE => []);
    76 
    76 
    77 fun specifications_of (Defs defs) = lookup_list (Inttab.dest o #specs) defs;
    77 fun specifications_of (Defs defs) = lookup_list (Inttab.dest o #specs) defs;
    78 val restricts_of = lookup_list #restricts;
    78 val restricts_of = lookup_list #restricts;
    79 val reducts_of = lookup_list #reducts;
    79 val reducts_of = lookup_list #reducts;