1signature TheoryReader =
2sig
3
4  exception TheoryReader of string
5  val load_thydata : string -> string -> (string, Thm.thm) Redblackmap.dict
6
7end
8
9(* [load_thydata thyname fname] loads the filename and makes the appropriate
10   changes to the theory hierarchy in response to the data stored there.  In
11   other words, this is done mostly for the side-effects. The map returned
12   allows <nm>Theory.sml files to then bind SML identifiers corresponding to
13   theorem names to theorem values.
14*)
15