src/LCF/ex/Ex3.thy

--- a/src/LCF/ex/Ex3.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/ex/Ex3.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -18,7 +18,7 @@
 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