src/LCF/ex/Ex3.thy

   p_s:          "p(s(x),y) = s(p(x,y))"
 
 declare p_strict [simp] p_s [simp]
 
 lemma example: "p(FIX(s),y) = FIX(s)"
-  apply (tactic {* induct_tac "s" 1 *})
+  apply (tactic {* induct_tac @{context} "s" 1 *})
   apply (simp (no_asm))
   apply (simp (no_asm))
   done
 
 end