--- 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)
--- 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;