src/Pure/sign.ML
changeset 1241 bfc93c86f0a1
parent 1239 2c0d94151e74
child 1393 73b6b003c6ca
equal deleted inserted replaced
1240:0901441a7ebf 1241:bfc93c86f0a1
    18        const_tab: typ Symtab.table,
    18        const_tab: typ Symtab.table,
    19        syn: syntax,
    19        syn: syntax,
    20        stamps: string ref list}
    20        stamps: string ref list}
    21     val subsig: sg * sg -> bool
    21     val subsig: sg * sg -> bool
    22     val eq_sg: sg * sg -> bool
    22     val eq_sg: sg * sg -> bool
       
    23     val same_sg: sg * sg -> bool
    23     val is_draft: sg -> bool
    24     val is_draft: sg -> bool
    24     val const_type: sg -> string -> typ option
    25     val const_type: sg -> string -> typ option
    25     val classes: sg -> class list
    26     val classes: sg -> class list
    26     val subsort: sg -> sort * sort -> bool
    27     val subsort: sg -> sort * sort -> bool
    27     val norm_sort: sg -> sort -> sort
    28     val norm_sort: sg -> sort -> sort
   105 
   106 
   106 fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
   107 fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
   107 
   108 
   108 fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
   109 fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
   109 
   110 
       
   111 (* test if same theory names are contained in signatures' stamps,
       
   112    i.e. if signatures belong to same theory but not necessarily to the same
       
   113    version of it*)
       
   114 fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
       
   115   eq_set (pairself (map (op !)) (s1, s2));
       
   116 
   110 
   117 
   111 (* consts *)
   118 (* consts *)
   112 
   119 
   113 fun const_type (Sg {const_tab, ...}) c =
   120 fun const_type (Sg {const_tab, ...}) c =
   114   Symtab.lookup (const_tab, c);
   121   Symtab.lookup (const_tab, c);