tuned comments;
authorwenzelm
Sat Oct 15 00:08:00 2005 +0200 (2005-10-15)
changeset 178512fa4f9b54761
parent 17850 6803625e71c4
child 17852 a06b185a26d7
tuned comments;
src/Pure/tactic.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/tactic.ML	Sat Oct 15 00:07:59 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Sat Oct 15 00:08:00 2005 +0200
     1.3 @@ -588,8 +588,6 @@
     1.4       Names may contain letters, digits or primes and must be
     1.5       separated by blanks ***)
     1.6  
     1.7 -(*Calling this will generate the warning "Same as previous level" since
     1.8 -  it affects nothing but the names of bound variables!*)
     1.9  fun rename_params_tac xs i =
    1.10    case Library.find_first (not o Syntax.is_identifier) xs of
    1.11        SOME x => error ("Not an identifier: " ^ x)
     2.1 --- a/src/Pure/term.ML	Sat Oct 15 00:07:59 2005 +0200
     2.2 +++ b/src/Pure/term.ML	Sat Oct 15 00:08:00 2005 +0200
     2.3 @@ -1220,7 +1220,7 @@
     2.4  fun term_frees t = add_term_frees(t,[]);
     2.5  
     2.6  (*Given an abstraction over P, replaces the bound variable by a Free variable
     2.7 -  having a unique name*)
     2.8 +  having a unique name -- SLOW!*)
     2.9  fun variant_abs (a,T,P) =
    2.10    let val b = variant (add_term_names(P,[])) a
    2.11    in  (b,  subst_bound (Free(b,T), P))  end;