src/HOL/Isar_examples/Hoare.thy

--- a/src/HOL/Isar_examples/Hoare.thy	Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy	Mon Sep 11 21:35:19 2006 +0200
@@ -167,7 +167,7 @@
   assume "Sem (While b X c) s s'"
   then obtain n where "iter n b (Sem c) s s'" by auto
   from this and s show "s' : P Int -b"
-  proof (induct n fixing: s)
+  proof (induct n arbitrary: s)
     case 0
     thus ?case by auto
   next