diff -r 548e2d3105b9 -r 5fe899199f85 src/LCF/ex/Ex4.thy
--- a/src/LCF/ex/Ex4.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/ex/Ex4.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -10,7 +10,7 @@
   shows "FIX(f)=p"
   apply (unfold eq_def)
   apply (rule conjI)
-  apply (tactic {* induct_tac "f" 1 *})
+  apply (tactic {* induct_tac @{context} "f" 1 *})
   apply (rule minimal)
   apply (intro strip)
   apply (rule less_trans)