TFL/tfl.sml
changeset 4252 d5ccc8321e1e
parent 4221 ed0f67fb458b
child 4857 cf554f1c65be
--- a/TFL/tfl.sml	Thu Nov 20 12:51:55 1997 +0100
+++ b/TFL/tfl.sml	Thu Nov 20 12:59:20 1997 +0100
@@ -335,7 +335,7 @@
      val wfrec_R_M =  map_term_types poly_tvars 
 	                  (wfrec $ map_term_types poly_tvars R) 
 	              $ functional
-     val (_, def_term, _) = 
+     val (def_term, _) = 
 	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
 	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
 		propT)