src/ZF/thy_data.ML
author paulson
Mon, 23 Sep 1996 17:42:56 +0200
changeset 2003 b48f066d52dc
parent 1903 591b76ead155
permissions -rw-r--r--
Addition of gensym
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