diff -r 259073d16f84 -r 188e2924433e src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Feb 22 21:49:34 2000 +0100
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Feb 22 21:50:02 2000 +0100
@@ -114,12 +114,12 @@
 lemma exec_append:
   "ALL stack. exec (xs @ ys) stack env =
     exec ys (exec xs stack env) env" (is "?P xs");
-proof (induct ?P xs type: list);
+proof (induct ?P xs in type: list);
   show "?P []"; by simp;
 
   fix x xs; assume "?P xs";
   show "?P (x # xs)" (is "?Q x");
-  proof (induct ?Q x type: instr);
+  proof (induct ?Q x in type: instr);
     show "!!val. ?Q (Const val)"; by (simp!);
     show "!!adr. ?Q (Load adr)"; by (simp!);
     show "!!fun. ?Q (Apply fun)"; by (simp!);
@@ -130,7 +130,7 @@
 proof -;
   have "ALL stack. exec (compile e) stack env =
     eval e env # stack" (is "?P e");
-  proof (induct ?P e type: expr);
+  proof (induct ?P e in type: expr);
     show "!!adr. ?P (Variable adr)"; by simp;
     show "!!val. ?P (Constant val)"; by simp;
     show "!!fun e1 e2. (?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2))";