
diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/ex/ReflectionEx.thy
--- a/src/HOL/ex/ReflectionEx.thy	Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/ex/ReflectionEx.thy	Mon Sep 11 21:35:19 2006 +0200
@@ -173,7 +173,7 @@
   "lin_mul t = (\<lambda> i. Mul i t)"
 
 lemma lin_mul: "Inum bs (lin_mul t i) = Inum bs (Mul i t)"
-by (induct t fixing: i rule: lin_mul.induct, auto simp add: ring_eq_simps)
+by (induct t arbitrary: i rule: lin_mul.induct) (auto simp add: ring_eq_simps)
 
 consts linum:: "num \<Rightarrow> num"
 recdef linum "measure num_size"




