Type inference makes a Const here, perhaps elsewhere?thry.sml
authorpaulson
Mon Jun 02 12:19:01 1997 +0200 (1997-06-02)
changeset 3388dbf61e36f8e9
parent 3387 6f2eaa0ce04b
child 3389 3150eba724a1
Type inference makes a Const here, perhaps elsewhere?thry.sml
TFL/tfl.sml
TFL/thry.sml
     1.1 --- a/TFL/tfl.sml	Mon Jun 02 12:17:19 1997 +0200
     1.2 +++ b/TFL/tfl.sml	Mon Jun 02 12:19:01 1997 +0200
     1.3 @@ -361,14 +361,6 @@
     1.4  					     quote fid ^ " but found one of " ^
     1.5  				      quote Name}
     1.6  		    else Name ^ "_def"
     1.7 -(****************????????????????
     1.8 -     val (_,ty_theta) = Thry.match_term thy f (S.mk_var{Name=fname,Ty=Ty})
     1.9 -     val wfrec' = S.inst ty_theta wfrec
    1.10 -     val wfrec_R_M' = list_comb(wfrec',[R,functional])
    1.11 -     val def_term = HOLogic.mk_eq(Bvar, wfrec_R_M')
    1.12 -
    1.13 -?? (map_term_types (incr_tvar 1) functional) ?? 
    1.14 -****************)
    1.15       val wfrec_R_M = map_term_types poly_tvars
    1.16  	               (wfrec $ R $ (map_term_types poly_tvars functional))
    1.17       val (_, def_term, _) = 
     2.1 --- a/TFL/thry.sml	Mon Jun 02 12:17:19 1997 +0200
     2.2 +++ b/TFL/thry.sml	Mon Jun 02 12:19:01 1997 +0200
     2.3 @@ -59,7 +59,7 @@
     2.4  in
     2.5  fun make_definition parent s tm = 
     2.6     let val {lhs,rhs} = S.dest_eq tm
     2.7 -       val (Name,Ty) = dest_Free lhs
     2.8 +       val (Name,Ty) = dest_Const lhs
     2.9         val lhs1 = S.mk_const{Name = Name, Ty = Ty}
    2.10         val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
    2.11         val dtm = list_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)