# HG changeset patch
# User paulson
# Date 864642550 -7200
# Node ID 3921ebbd9cf0992a3abfca427934758cd0835e3f
# Parent  c81c7f8ad333e56730f80ef4794df3db29beb2ba
More de-HOL-ification

diff -r c81c7f8ad333 -r 3921ebbd9cf0 TFL/rules.new.sml
--- 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
diff -r c81c7f8ad333 -r 3921ebbd9cf0 TFL/thry.sml
--- 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 "==" *)