# HG changeset patch
# User paulson
# Date 825504368 -3600
# Node ID 7513fbe502fb7170b0a7fa078cf3453ab1240fe5
# Parent  4093c3cb7b30188537250a5f78500e86584e3c10
changed prove_goal to qed_goal

diff -r 4093c3cb7b30 -r 7513fbe502fb 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) ]);