diff -r 9be9e39fd862 -r 96fba19bcbe2 src/HOL/W0/MiniML.ML
--- a/src/HOL/W0/MiniML.ML	Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/W0/MiniML.ML	Mon Nov 03 12:13:18 1997 +0100
@@ -14,11 +14,11 @@
 goal MiniML.thy "!!a e t. 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);
+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);
+by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
 (* case AppI *)
 by (Asm_full_simp_tac 1);
 qed "has_type_cl_sub";