src/FOL/ROOT.ML

--- a/src/FOL/ROOT.ML	Tue Feb 27 19:08:36 1996 +0100
+++ b/src/FOL/ROOT.ML	Wed Feb 28 11:46:08 1996 +0100
@@ -63,7 +63,7 @@
 val FOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] 
                      addSEs [exE,ex1E] addEs [allE];
 
-val ex1_functional = prove_goal FOL.thy
+qed_goal "ex1_functional" FOL.thy
     "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
  (fn _ => [ (deepen_tac FOL_cs 0 1) ]);