diff -r bb9dad7de515 -r 51829fe604a7 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Jan 15 08:27:21 2010 +0100
+++ b/src/HOL/Code_Numeral.thy	Fri Jan 15 14:43:00 2010 +0100
@@ -83,7 +83,7 @@
     then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
     then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
   from init step have "P (of_nat (nat_of k))"
-    by (induct "nat_of k") simp_all
+    by (induct ("nat_of k")) simp_all
   then show "P k" by simp
 qed simp_all
 
@@ -100,7 +100,7 @@
   fix k
   have "code_numeral_size k = nat_size (nat_of k)"
     by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
-  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
+  also have "nat_size (nat_of k) = nat_of k" by (induct ("nat_of k")) simp_all
   finally show "code_numeral_size k = nat_of k" .
 qed