src/HOL/TLA/Action.ML

          Const("Intensional.TrueInt",_) $ p 
            => (action_unlift th
                   handle _ => int_unlift th)
        | _ => th);
 
-simpset := !simpset setmksimps ((mksimps mksimps_pairs) o maybe_unlift);
+simpset_ref() := simpset() setmksimps ((mksimps mksimps_pairs) o maybe_unlift);
 
 (* make act_rews be always active -- intensional_rews has been added before *)
 Addsimps act_rews;
 
 use "cladata.ML";        (* local version! *)

     (asm_full_simp_tac 
          (ss setloop ((resolve_tac (intros @ [refl,impI,conjI,actionI,allI]))
 		      ORELSE' (eresolve_tac (elims @ [conjE,disjE,exE_prop]))))
          i);
 (* default version without additional plug-in rules *)
-fun Action_simp_tac i = (action_simp_tac (!simpset) [] [] i);
+fun Action_simp_tac i = (action_simp_tac (simpset()) [] [] i);
 
 
 (* ==================== Simplification of abstractions ==================== *)
 
 (* Somewhat obscure simplifications, rarely necessary to get rid