--- a/TFL/thms.sml Thu May 15 11:35:26 1997 +0200
+++ b/TFL/thms.sml Thu May 15 12:29:59 1997 +0200
@@ -2,9 +2,9 @@
struct
type Thm = Thm.thm
- val WFREC_COROLLARY = get_thm WF1.thy "tfl_wfrec"
- val WF_INDUCTION_THM = get_thm WF1.thy "tfl_wf_induct"
- val CUT_LEMMA = get_thm WF1.thy "tfl_cut_apply"
+ 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"
val CUT_DEF = cut_def
local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"