src/HOL/String.thy

--- a/src/HOL/String.thy	Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/String.thy	Mon Jul 27 17:44:55 2015 +0200
@@ -253,7 +253,7 @@
     put_simpset HOL_ss @{context}
       addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
   fun mk_code_eqn x y =
-    Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
+    Thm.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
     |> simplify simpset;
   val code_eqns = map_product mk_code_eqn nibbles nibbles;
 in