TFL/tfl.sml
changeset 3388 dbf61e36f8e9
parent 3387 6f2eaa0ce04b
child 3391 5e45dd3b64e9
--- a/TFL/tfl.sml	Mon Jun 02 12:17:19 1997 +0200
+++ b/TFL/tfl.sml	Mon Jun 02 12:19:01 1997 +0200
@@ -361,14 +361,6 @@
 					     quote fid ^ " but found one of " ^
 				      quote Name}
 		    else Name ^ "_def"
-(****************????????????????
-     val (_,ty_theta) = Thry.match_term thy f (S.mk_var{Name=fname,Ty=Ty})
-     val wfrec' = S.inst ty_theta wfrec
-     val wfrec_R_M' = list_comb(wfrec',[R,functional])
-     val def_term = HOLogic.mk_eq(Bvar, wfrec_R_M')
-
-?? (map_term_types (incr_tvar 1) functional) ?? 
-****************)
      val wfrec_R_M = map_term_types poly_tvars
 	               (wfrec $ R $ (map_term_types poly_tvars functional))
      val (_, def_term, _) =