# HG changeset patch
# User wenzelm
# Date 1129327680 -7200
# Node ID 2fa4f9b547619e07b8c950ab7d3f0afe744e716e
# Parent  6803625e71c4f27cea73b39d96032962e022afaf
tuned comments;

diff -r 6803625e71c4 -r 2fa4f9b54761 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sat Oct 15 00:07:59 2005 +0200
+++ b/src/Pure/tactic.ML	Sat Oct 15 00:08:00 2005 +0200
@@ -588,8 +588,6 @@
      Names may contain letters, digits or primes and must be
      separated by blanks ***)
 
-(*Calling this will generate the warning "Same as previous level" since
-  it affects nothing but the names of bound variables!*)
 fun rename_params_tac xs i =
   case Library.find_first (not o Syntax.is_identifier) xs of
       SOME x => error ("Not an identifier: " ^ x)
diff -r 6803625e71c4 -r 2fa4f9b54761 src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Oct 15 00:07:59 2005 +0200
+++ b/src/Pure/term.ML	Sat Oct 15 00:08:00 2005 +0200
@@ -1220,7 +1220,7 @@
 fun term_frees t = add_term_frees(t,[]);
 
 (*Given an abstraction over P, replaces the bound variable by a Free variable
-  having a unique name*)
+  having a unique name -- SLOW!*)
 fun variant_abs (a,T,P) =
   let val b = variant (add_term_names(P,[])) a
   in  (b,  subst_bound (Free(b,T), P))  end;