# HG changeset patch # User lcp # Date 785633435 -3600 # Node ID 435ff9ec4058a4facdaea299b4a8a0e75d8b2a59 # Parent 15c822377c18da1a8bc18827f81368f25da65a78 trivial changes 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";