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