--- a/src/HOL/Univ.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/Univ.ML Fri Apr 11 15:21:36 1997 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/univ
+(* Title: HOL/Univ
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -147,7 +147,7 @@
qed "Scons_inject_lemma1";
goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
-by (fast_tac (!claset addSDs [Push_Node_inject]) 1);
+by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
qed "Scons_inject_lemma2";
val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";