diff -r 3c94c44dfc0f -r 4517e9a96ace src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Mar 04 20:16:39 2015 +0100
+++ b/src/Pure/tactic.ML	Wed Mar 04 20:47:29 2015 +0100
@@ -294,7 +294,7 @@
 
 (*Renaming of parameters in a subgoal*)
 fun rename_tac xs i =
-  case Library.find_first (not o Symbol_Pos.is_identifier) xs of
+  case find_first (not o Symbol_Pos.is_identifier) xs of
       SOME x => error ("Not an identifier: " ^ x)
     | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i));