More de-HOL-ification
authorpaulson
Mon May 26 12:29:10 1997 +0200 (1997-05-26)
changeset 33323921ebbd9cf0
parent 3331 c81c7f8ad333
child 3333 0bbf06e86c06
More de-HOL-ification
TFL/rules.new.sml
TFL/thry.sml
     1.1 --- a/TFL/rules.new.sml	Mon May 26 12:28:30 1997 +0200
     1.2 +++ b/TFL/rules.new.sml	Mon May 26 12:29:10 1997 +0200
     1.3 @@ -504,7 +504,7 @@
     1.4              let val eq = Logic.strip_imp_concl body
     1.5                  val (f,args) = S.strip_comb (get_lhs eq)
     1.6                  val (vstrl,_) = S.strip_abs f
     1.7 -                val names  = map (#Name o S.dest_var)
     1.8 +                val names  = map (#1 o dest_Free)
     1.9                                   (variants (S.free_vars body) vstrl)
    1.10              in get (rst, n+1, (names,n)::L)
    1.11              end handle _ => get (rst, n+1, L);
    1.12 @@ -594,7 +594,7 @@
    1.13  in
    1.14  fun XFILL tych x vstruct = 
    1.15    let fun traverse p xocc L =
    1.16 -        if (S.is_var p)
    1.17 +        if (is_Free p)
    1.18          then tych xocc::L
    1.19          else let val (p1,p2) = dest_pair p
    1.20               in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
    1.21 @@ -626,7 +626,7 @@
    1.22        val vstr1 = tych vstr
    1.23    in
    1.24    forall_intr a1 
    1.25 -     (if (S.is_var vstr) 
    1.26 +     (if (is_Free vstr) 
    1.27        then cterm_instantiate [(vstr1,a1)] th
    1.28        else VSTRUCT_ELIM tych a vstr th)
    1.29    end;
    1.30 @@ -766,10 +766,9 @@
    1.31                 * term "f v1..vn" which is a pattern that any full application
    1.32                 * of "f" will match.
    1.33                 *-------------------------------------------------------------*)
    1.34 -              val func_name = #Name(S.dest_const func handle _ => 
    1.35 -                                    S.dest_var func)
    1.36 -              fun is_func tm = (#Name(S.dest_const tm handle _ =>
    1.37 -                                      S.dest_var tm) = func_name)
    1.38 +              val func_name = #1(dest_Const func handle _ => dest_Free func)
    1.39 +              fun is_func tm = (#1(dest_Const tm handle _ => dest_Free tm) 
    1.40 +				= func_name)
    1.41                                 handle _ => false
    1.42                val nested = U.can(S.find_term is_func)
    1.43                val rcontext = rev cntxt
     2.1 --- a/TFL/thry.sml	Mon May 26 12:28:30 1997 +0200
     2.2 +++ b/TFL/thry.sml	Mon May 26 12:29:10 1997 +0200
     2.3 @@ -64,7 +64,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} = S.dest_var lhs
     2.8 +       val (Name,Ty) = dest_Free 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 "==" *)