src/FOL/thy_data.ML
author wenzelm
Tue, 27 May 1997 15:45:07 +0200
changeset 3362 0b268cff9344
parent 2469 b50b8c0eec01
permissions -rw-r--r--
NJ 1.09.2x as factory default!

(*  Title:      FOL/thy_data.ML
    ID:         $Id$
    Author:     Carsten Clasohm
    Copyright   1995 TU Muenchen

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

fun simpset_of tname =
  case get_thydata tname "simpset" of
      None => empty_ss
    | Some (SS_DATA ss) => ss;

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