# HG changeset patch
# User paulson
# Date 920456830 -3600
# Node ID 5e0b1ad1a4471d3cc8f1567b0920af78d6e4613c
# Parent  957d8e203be10230a514d8ed14c7631edf1282fc
expandshort

diff -r 957d8e203be1 -r 5e0b1ad1a447 src/HOL/W0/Type.ML
--- 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];