src/ZF/ex/Limit.ML

--- a/src/ZF/ex/Limit.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/ex/Limit.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -2317,7 +2317,7 @@
 
 val prems = Goalw [mediating_def]
   "[|emb(E,G,t);  !!n. n \\<in> nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)";
-by (Safe_tac);
+by Safe_tac;
 by (REPEAT (ares_tac prems 1));
 qed "mediatingI";