src/HOL/MiniML/MiniML.ML

--- a/src/HOL/MiniML/MiniML.ML	Wed Feb 28 11:47:30 1996 +0100
+++ b/src/HOL/MiniML/MiniML.ML	Wed Feb 28 16:57:14 1996 +0100
@@ -12,7 +12,7 @@
 
 (* has_type is closed w.r.t. substitution *)
 goal MiniML.thy
-     "!a e t. (a |- e :: t) --> ($ s a |- e :: $ s t)";
+     "!a e t. a |- e :: t --> $s a |- e :: $s t";
 by (rtac has_type.mutual_induct 1);
 (* case VarI *)
 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);