--- a/TFL/tfl.sml Fri May 30 15:30:52 1997 +0200
+++ b/TFL/tfl.sml Fri May 30 15:55:27 1997 +0200
@@ -426,9 +426,9 @@
val (case_rewrites,context_congs) = extraction_thms theory
val corollaries' = map(R.simplify case_rewrites) corollaries
fun xtract th = R.CONTEXT_REWRITE_RULE(f,R)
- {thms = [(R.ISPECL o map tych)[f,R] Thms.CUT_LEMMA],
- congs = context_congs,
- th = th}
+ {cut_lemma = R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
+ congs = context_congs,
+ th = th}
val (rules, TCs) = ListPair.unzip (map xtract corollaries')
val rules0 = map (R.simplify [Thms.CUT_DEF]) rules
val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR)
@@ -464,9 +464,9 @@
val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
val corollaries' = map (R.simplify case_rewrites) corollaries
fun extract th = R.CONTEXT_REWRITE_RULE(f,R1)
- {thms = [(R.ISPECL o map tych)[f,R1] Thms.CUT_LEMMA],
- congs = context_congs,
- th = th}
+ {cut_lemma = R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA,
+ congs = context_congs,
+ th = th}
in {proto_def=proto_def,
WFR=WFR,
pats=pats,