src/Doc/ZF/IFOL_examples.thy

--- a/src/Doc/ZF/IFOL_examples.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/Doc/ZF/IFOL_examples.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -36,7 +36,7 @@
 done
 
 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
-by (tactic {*IntPr.fast_tac 1*})
+by (tactic {*IntPr.fast_tac @{context} 1*})
 
 text{*Example of Dyckhoff's method*}
 lemma "~ ~ ((P-->Q) | (Q-->P))"