src/HOL/thy_data.ML
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1465 5d7a7e439cec
child 1657 a7a6c3fb3cdd
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
     1 (*  Title:      HOL/thy_data.ML
     2     ID:         $Id$
     3     Author:     Carsten Clasohm
     4     Copyright   1995 TU Muenchen
     5 
     6 Definitions that have to be reread after init_thy_reader has been invoked
     7 *)
     8 
     9 fun simpset_of tname =
    10   case get_thydata (theory_of tname) "simpset" of
    11       None => empty_ss
    12     | Some (SS_DATA ss) => ss;
    13 
    14 fun datatypes_of tname =
    15   case get_thydata (theory_of tname) "datatypes" of
    16       None => []
    17     | Some (DT_DATA ds) => ds;