--- 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