diff -r 15c822377c18 -r 435ff9ec4058 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Wed Nov 23 11:45:56 1994 +0100
+++ b/src/FOL/ROOT.ML	Thu Nov 24 00:30:35 1994 +0100
@@ -64,7 +64,7 @@
 
 val ex1_functional = prove_goal FOL.thy
     "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
- (fn _ => [ (deepen_tac FOL_cs 1 1) ]);
+ (fn _ => [ (deepen_tac FOL_cs 0 1) ]);
 
 use "simpdata.ML";