src/ZF/thy_data.ML
author wenzelm
Mon, 09 Dec 1996 09:03:52 +0100
changeset 2334 00db792beb4e
parent 1903 591b76ead155
permissions -rw-r--r--
added -norc option; error output to stderr;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1903
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
     1
(*  Title:      ZF/thy_data.ML
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
     2
    ID:         $Id$
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
     4
    Copyright   1996 TU Muenchen
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
     5
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
     6
Definitions that have to be reread after init_thy_reader has been invoked
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
     7
*)
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
     8
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
     9
fun claset_of tname =
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
    10
  case get_thydata tname "claset" of
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
    11
      None => empty_cs
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
    12
    | Some (CS_DATA cs) => cs;
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
    13
591b76ead155 Initial revision of thy_data.ML
berghofe
parents:
diff changeset
    14