--- a/TFL/rules.new.sml Mon May 26 12:28:30 1997 +0200
+++ b/TFL/rules.new.sml Mon May 26 12:29:10 1997 +0200
@@ -504,7 +504,7 @@
let val eq = Logic.strip_imp_concl body
val (f,args) = S.strip_comb (get_lhs eq)
val (vstrl,_) = S.strip_abs f
- val names = map (#Name o S.dest_var)
+ val names = map (#1 o dest_Free)
(variants (S.free_vars body) vstrl)
in get (rst, n+1, (names,n)::L)
end handle _ => get (rst, n+1, L);
@@ -594,7 +594,7 @@
in
fun XFILL tych x vstruct =
let fun traverse p xocc L =
- if (S.is_var p)
+ if (is_Free p)
then tych xocc::L
else let val (p1,p2) = dest_pair p
in traverse p1 (mk_fst xocc) (traverse p2 (mk_snd xocc) L)
@@ -626,7 +626,7 @@
val vstr1 = tych vstr
in
forall_intr a1
- (if (S.is_var vstr)
+ (if (is_Free vstr)
then cterm_instantiate [(vstr1,a1)] th
else VSTRUCT_ELIM tych a vstr th)
end;
@@ -766,10 +766,9 @@
* term "f v1..vn" which is a pattern that any full application
* of "f" will match.
*-------------------------------------------------------------*)
- val func_name = #Name(S.dest_const func handle _ =>
- S.dest_var func)
- fun is_func tm = (#Name(S.dest_const tm handle _ =>
- S.dest_var tm) = func_name)
+ val func_name = #1(dest_Const func handle _ => dest_Free func)
+ fun is_func tm = (#1(dest_Const tm handle _ => dest_Free tm)
+ = func_name)
handle _ => false
val nested = U.can(S.find_term is_func)
val rcontext = rev cntxt
--- a/TFL/thry.sml Mon May 26 12:28:30 1997 +0200
+++ b/TFL/thry.sml Mon May 26 12:29:10 1997 +0200
@@ -64,7 +64,7 @@
in
fun make_definition parent s tm =
let val {lhs,rhs} = S.dest_eq tm
- val {Name,Ty} = S.dest_var lhs
+ val (Name,Ty) = dest_Free 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 "==" *)