src/HOL/MiniML/MiniML.ML
changeset 2031 03a843f0f447
parent 1743 f7feaacd33d3
child 2525 477c05586286
--- a/src/HOL/MiniML/MiniML.ML	Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/MiniML/MiniML.ML	Thu Sep 26 12:47:47 1996 +0200
@@ -16,7 +16,7 @@
 (* case VarI *)
 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
 by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
-by( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1);
+by ( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1);
 (* case AbsI *)
 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
 (* case AppI *)