src/Pure/Thy/thm_database.ML
changeset 1580 e3fd931e6095
parent 1512 ce37c64244c0
child 1654 faa643c33ee6
equal deleted inserted replaced
1579:688e18023915 1580:e3fd931e6095
    84                else update_db true
    84                else update_db true
    85                       cs (Symtab.update ((c, tagged_thm :: old_thms), result))
    85                       cs (Symtab.update ((c, tagged_thm :: old_thms), result))
    86             end;
    86             end;
    87 
    87 
    88       val const_idx' = update_db false consts const_idx;
    88       val const_idx' = update_db false consts const_idx;
    89   in if consts = [] then writeln ("Warning: Theorem " ^ name ^
    89   in if consts = [] then warning ("Theorem " ^ name ^
    90                                   " cannot be stored in ThmDB\n\t because it \
    90                                   " cannot be stored in ThmDB\n\t because it \
    91                                   \contains no or only ignored constants.")
    91                                   \contains no or only ignored constants.")
    92      else if is_some const_idx' then
    92      else if is_some const_idx' then
    93        thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx,
    93        thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx,
    94                         const_idx = the const_idx'}
    94                         const_idx = the const_idx'}