# 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 "==" *)