# HG changeset patch
# User paulson
# Date 826549689 -3600
# Node ID 717f8816eca5d9250ea2a039a2d4d92473a9d918
# Parent  e98c7f6165c9610ef5dd4a8ab6a089139c170488
New, one-line proof of inj_Atom

diff -r e98c7f6165c9 -r 717f8816eca5 src/HOL/Univ.ML
--- 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;