--- a/TFL/tfl.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/TFL/tfl.ML Fri Sep 15 22:56:13 2006 +0200
@@ -389,8 +389,8 @@
quote fid ^ " but found one of " ^
quote x)
else x ^ "_def"
- val wfrec_R_M = map_term_types poly_tvars
- (wfrec $ map_term_types poly_tvars R)
+ val wfrec_R_M = map_types poly_tvars
+ (wfrec $ map_types poly_tvars R)
$ functional
val def_term = mk_const_def (Theory.sign_of thy) (x, Ty, wfrec_R_M)
val ([def], thy') = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy