src/FOL/thy_data.ML
author paulson
Fri, 31 Jan 1997 17:13:19 +0100
changeset 2572 8a47f85e7a03
parent 2469 b50b8c0eec01
permissions -rw-r--r--
ex_impE was incorrectly listed as Safe

(*  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;