# HG changeset patch
# User paulson
# Date 1149166297 -7200
# Node ID b345d4e70ca9edd6c4476c203563e8acd5b1ef64
# Parent  18e5aa65fb8b53af13e3bbade5909ef0a0c6644b
Tiny code cleanup

diff -r 18e5aa65fb8b -r b345d4e70ca9 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jun 01 14:40:22 2006 +0200
+++ b/src/Pure/drule.ML	Thu Jun 01 14:51:37 2006 +0200
@@ -474,10 +474,8 @@
    case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
        [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
      | vars =>
-         let fun newName (Var(ix,_), pairs) =
-                   let val v = gensym (string_of_indexname ix)
-                   in  ((ix,v)::pairs)  end;
-             val alist = foldr newName [] vars
+         let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix))
+             val alist = map newName vars
              fun mk_inst (Var(v,T)) =
                  (cterm_of thy (Var(v,T)),
                   cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
@@ -489,7 +487,8 @@
  end;
 
 (*Basic version of the function above. No option to rename Vars apart in thaw.
-  The Frees created from Vars have nice names.*)
+  The Frees created from Vars have nice names. FIXME: does not check for 
+  clashes with variables in the assumptions, so delete and use freeze_thaw_robust instead?*)
 fun freeze_thaw th =
  let val fth = freezeT th
      val {prop, tpairs, thy, ...} = rep_thm fth