TFL/tfl.sml
changeset 3379 7091ffa99c93
parent 3353 9112a2efb9a3
child 3387 6f2eaa0ce04b
--- 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,