New, one-line proof of inj_Atom

--- a/src/HOL/Univ.ML	Mon Mar 11 14:05:45 1996 +0100
+++ b/src/HOL/Univ.ML	Mon Mar 11 14:08:09 1996 +0100
@@ -99,10 +99,8 @@
 
 (** Atomic nodes **)
 
-goalw Univ.thy [Atom_def] "inj(Atom)";
-by (rtac injI 1);
-by (etac (singleton_inject RS Abs_Node_inject RS Pair_inject) 1);
-by (REPEAT (ares_tac [Node_K0_I] 1));
+goalw Univ.thy [Atom_def, inj_def] "inj(Atom)";
+by (fast_tac (prod_cs addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
 qed "inj_Atom";
 val Atom_inject = inj_Atom RS injD;