TFL/thms.sml
changeset 3245 241838c01caf
parent 3191 14bd6e5985f1
child 3273 114704740c86
--- a/TFL/thms.sml	Tue May 20 11:47:33 1997 +0200
+++ b/TFL/thms.sml	Tue May 20 11:49:57 1997 +0200
@@ -1,7 +1,5 @@
 structure Thms : Thms_sig =
 struct
-   type Thm = Thm.thm
-
    val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"
    val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct"
    val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply"