# HG changeset patch
# User paulson
# Date 865246741 -7200
# Node ID dbf61e36f8e99138415c08d806af79fabe83cb04
# Parent  6f2eaa0ce04bbf74d6bb62ded67fc58f94705625
Type inference makes a Const here, perhaps elsewhere?thry.sml

diff -r 6f2eaa0ce04b -r dbf61e36f8e9 TFL/tfl.sml
--- 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, _) = 
diff -r 6f2eaa0ce04b -r dbf61e36f8e9 TFL/thry.sml
--- a/TFL/thry.sml	Mon Jun 02 12:17:19 1997 +0200
+++ b/TFL/thry.sml	Mon Jun 02 12:19:01 1997 +0200
@@ -59,7 +59,7 @@
 in
 fun make_definition parent s tm = 
    let val {lhs,rhs} = S.dest_eq tm
-       val (Name,Ty) = dest_Free lhs
+       val (Name,Ty) = dest_Const lhs
        val lhs1 = S.mk_const{Name = Name, Ty = Ty}
        val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
        val dtm = list_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)