src/Pure/tactic.ML
changeset 13559 51c3ac47d127
parent 13105 3d1e7a199bdc
child 13650 31bd2a8cdbe2
     1.1 --- a/src/Pure/tactic.ML	Tue Sep 03 18:49:30 2002 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Sep 05 14:03:03 2002 +0200
     1.3 @@ -560,10 +560,13 @@
     1.4  (*Calling this will generate the warning "Same as previous level" since
     1.5    it affects nothing but the names of bound variables!*)
     1.6  fun rename_params_tac xs i =
     1.7 -  (if !Logic.auto_rename
     1.8 -    then (warning "Resetting Logic.auto_rename";
     1.9 -        Logic.auto_rename := false)
    1.10 -   else (); PRIMITIVE (rename_params_rule (xs, i)));
    1.11 +  case Library.find_first (not o Symbol.is_identifier) xs of
    1.12 +      Some x => error ("Not an identifier: " ^ x)
    1.13 +    | None => 
    1.14 +       (if !Logic.auto_rename
    1.15 +	 then (warning "Resetting Logic.auto_rename";
    1.16 +	     Logic.auto_rename := false)
    1.17 +	else (); PRIMITIVE (rename_params_rule (xs, i)));
    1.18  
    1.19  fun rename_tac str i =
    1.20    let val cs = Symbol.explode str in