src/HOL/W0/MiniML.ML

--- a/src/HOL/W0/MiniML.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/W0/MiniML.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -11,7 +11,7 @@
 
 
 (* has_type is closed w.r.t. substitution *)
-Goal "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
+Goal "a |- e :: t ==> $s a |- e :: $s t";
 by (etac has_type.induct 1);
 (* case VarI *)
 by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);