expandshort

--- a/src/HOL/W0/Type.ML	Wed Mar 03 11:26:36 1999 +0100
+++ b/src/HOL/W0/Type.ML	Wed Mar 03 11:27:10 1999 +0100
@@ -212,7 +212,7 @@
 Goal "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
 by (simp_tac (simpset() addsimps [new_tv_list]) 1);
 by (induct_tac "ts" 1);
-by (Safe_tac);
+by Safe_tac;
 by    (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
 qed_spec_mp "new_tv_subst_tel";
 Addsimps [new_tv_subst_tel];