# HG changeset patch
# User paulson
# Date 865246639 -7200
# Node ID 6f2eaa0ce04bbf74d6bb62ded67fc58f94705625
# Parent  2a2def2ac317a6cc27b41f285b23e21eb78180a5
poly_tvars allows recdefs to be made without type constraints

diff -r 2a2def2ac317 -r 6f2eaa0ce04b TFL/tfl.sml
--- 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