diff -r 9be9e39fd862 -r 96fba19bcbe2 src/HOL/TLA/Memory/Memory.ML
--- a/src/HOL/TLA/Memory/Memory.ML	Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/TLA/Memory/Memory.ML	Mon Nov 03 12:13:18 1997 +0100
@@ -19,7 +19,7 @@
 val UM_temp_defs = [UPSpec_def, MSpec_def, IUSpec_def];
 
 (* Make sure the simpset accepts non-boolean simplifications *)
-simpset := !simpset setmksimps ((mksimps mksimps_pairs) o maybe_unlift);
+simpset_ref() := simpset() setmksimps ((mksimps mksimps_pairs) o maybe_unlift);
 
 (* -------------------- Proofs -------------------------------------------------- *)
 
@@ -33,7 +33,7 @@
 (* The memory spec implies the memory invariant *)
 qed_goal "MemoryInvariant" Memory.thy 
    "(MSpec ch mm rs l) .-> []($(MemInv mm l))"
-   (fn _ => [ auto_inv_tac (!simpset addsimps RM_temp_defs @ MP_simps @ RM_action_defs) 1 ]);
+   (fn _ => [ auto_inv_tac (simpset() addsimps RM_temp_defs @ MP_simps @ RM_action_defs) 1 ]);
 
 (* The invariant is trivial for non-locations *)
 qed_goal "NonMemLocInvariant" Memory.thy
@@ -69,8 +69,8 @@
    "!!p. base_var <rtrner ch @ p, rs@p> ==> \
 \        $(Calling ch p) .& ($(rs@p) .~= #NotAResult) \
 \        .-> $(Enabled (<MemReturn ch rs p>_<rtrner ch @ p, rs@p>))"
-   (fn _ => [action_simp_tac (!simpset) [MemReturn_change RSN (2,enabled_mono)] [] 1,
-             action_simp_tac (!simpset addsimps [MemReturn_def,Return_def,rtrner_def])
+   (fn _ => [action_simp_tac (simpset()) [MemReturn_change RSN (2,enabled_mono)] [] 1,
+             action_simp_tac (simpset() addsimps [MemReturn_def,Return_def,rtrner_def])
                              [] [base_enabled,Pair_inject] 1
 	    ]);
 
@@ -83,7 +83,7 @@
 	     case_tac "MemLoc l" 1,
              ALLGOALS
 	        (action_simp_tac 
-                    (!simpset addsimps [ReadInner_def,GoodRead_def,BadRead_def,
+                    (simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,
 					RdRequest_def])
                     [] [base_enabled,Pair_inject])
             ]);
@@ -96,7 +96,7 @@
 	     case_tac "MemLoc l & MemVal v" 1,
              ALLGOALS
 	        (action_simp_tac 
-                    (!simpset addsimps [WriteInner_def,GoodWrite_def,BadWrite_def,
+                    (simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def,
 					WrRequest_def])
                     [] [base_enabled,Pair_inject])
             ]);
@@ -104,7 +104,7 @@
 qed_goal "ReadResult" Memory.thy
    "(Read ch mm rs p) .& (RALL l. $(MemInv mm l)) .-> (rs@p)$ .~= #NotAResult"
    (fn _ => [action_simp_tac 
-               (!simpset addsimps (MP_simps 
+               (simpset() addsimps (MP_simps 
 				   @ [Read_def,ReadInner_def,GoodRead_def,
 				      BadRead_def,MemInv_def]))
 	       [] [] 1,
@@ -112,8 +112,8 @@
 
 qed_goal "WriteResult" Memory.thy
    "(Write ch mm rs p l) .-> (rs@p)$ .~= #NotAResult"
-   (fn _ => [auto_tac (!claset,
-		       !simpset addsimps (MP_simps @
+   (fn _ => [auto_tac (claset(),
+		       simpset() addsimps (MP_simps @
 				   [Write_def,WriteInner_def,GoodWrite_def,BadWrite_def]))
 	    ]);
 
@@ -146,14 +146,14 @@
    (fn _ => [auto_tac (action_css addsimps2 [enabled_disj]
 		                  addSIs2 [action_mp RWRNext_enabled]),
 	     res_inst_tac [("s","arg(ch s p)")] sumE 1,
-	     action_simp_tac (!simpset addsimps [Read_def,enabled_ex,base_pair])
+	     action_simp_tac (simpset() addsimps [Read_def,enabled_ex,base_pair])
 	                     [action_mp ReadInner_enabled,exI] [] 1,
 	     split_all_tac 1, Rd.induct_tac "xa" 1,
 	     (* introduce a trivial subgoal to solve flex-flex constraint?! *)
 	     subgoal_tac "y = snd(xa,y)" 1,
 	     TRYALL Simp_tac,  (* solves "read" case *)
 	     etac swap 1,
-	     action_simp_tac (!simpset addsimps [Write_def,enabled_ex,base_pair])
+	     action_simp_tac (simpset() addsimps [Write_def,enabled_ex,base_pair])
 	                     [action_mp WriteInner_enabled,exI] [] 1,
 	     split_all_tac 1, Wr.induct_tac "x" 1,
 	     subgoal_tac "(xa = fst(snd(x,xa,y))) & (y = snd(snd(x,xa,y)))" 1,