| changeset 33038 | 8f9594c31de4 | 
| parent 33037 | b22e44496dc2 | 
| child 33049 | c38f02fdf35d | 
--- a/src/Pure/thm.ML Tue Oct 20 16:13:01 2009 +0200 +++ b/src/Pure/thm.ML Wed Oct 21 08:14:38 2009 +0200 @@ -1463,7 +1463,7 @@ (case duplicates (op =) cs of a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); state) | [] => - (case gen_inter (op =) (cs, freenames) of + (case inter (op =) (cs, freenames) of a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); state) | [] => Thm (der,