diff -r 46048223e0f9 -r b46ccfee8e59 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Wed Jul 14 13:32:21 1999 +0200
+++ b/src/HOL/cladata.ML	Thu Jul 15 10:27:54 1999 +0200
@@ -53,15 +53,15 @@
 claset_ref() := HOL_cs;
 
 (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
-qed_goal "alt_ex1E" thy
+val major::prems = goal thy
     "[| ?! x. P(x);                                              \
 \       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
-\    |] ==> R"
- (fn major::prems =>
-  [ (rtac (major RS ex1E) 1),
-    (REPEAT (ares_tac (allI::prems) 1)),
-    (etac (dup_elim allE) 1),
-    (Fast_tac 1)]);
+\    |] ==> R";
+by (rtac (major RS ex1E) 1);
+by (REPEAT (ares_tac (allI::prems) 1));
+by (etac (dup_elim allE) 1);
+by (Fast_tac 1);
+qed "alt_ex1E";
 
 AddSEs [alt_ex1E];