diff -r 5b026cfc5f04 -r 2a683fb686fd src/LCF/ex/Ex3.thy
--- a/src/LCF/ex/Ex3.thy	Tue Nov 11 11:41:58 2014 +0100
+++ b/src/LCF/ex/Ex3.thy	Tue Nov 11 11:47:53 2014 +0100
@@ -14,7 +14,7 @@
 declare p_strict [simp] p_s [simp]
 
 lemma example: "p(FIX(s),y) = FIX(s)"
-  apply (tactic {* induct_tac @{context} "s" 1 *})
+  apply (induct s)
   apply simp
   apply simp
   done