--- a/TFL/tfl.sml Mon Jun 02 12:16:24 1997 +0200
+++ b/TFL/tfl.sml Mon Jun 02 12:17:19 1997 +0200
@@ -337,6 +337,12 @@
*---------------------------------------------------------------------------*)
+(*Make all TVars available for instantiation by adding a ? to the front*)
+fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
+ | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
+ | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
+
+
(*---------------------------------------------------------------------------
* R is already assumed to be type-copacetic with M
*---------------------------------------------------------------------------*)
@@ -355,17 +361,21 @@
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')
-(****************????????????????
- val wfrec_R_M = wfrec $ R $ functional
+
+?? (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, _) =
Sign.infer_types (sign_of thy) (K None) (K None) [] false
- ([HOLogic.mk_eq(Bvar, wfrec_R_M)], HOLogic.boolT)
+ ([HOLogic.mk_eq(Bvar, wfrec_R_M)],
+ HOLogic.boolT)
-****************)
in
Thry.make_definition thy def_name def_term
end