src/ZF/thy_data.ML

Removed some dead wood. Transferred lemmas used to prove analz_image_newK
to Shared.ML

(*  Title:      ZF/thy_data.ML
    ID:         $Id$
    Author:     Stefan Berghofer
    Copyright   1996 TU Muenchen

Definitions that have to be reread after init_thy_reader has been invoked
*)

fun claset_of tname =
  case get_thydata tname "claset" of
      None => empty_cs
    | Some (CS_DATA cs) => cs;