src/Provers/classical.ML

   val global_claset_of  : theory -> claset
   val claset_of         : Proof.context -> claset
 
   val fast_tac          : claset -> int -> tactic
   val slow_tac          : claset -> int -> tactic
-  val weight_ASTAR      : int ref
+  val weight_ASTAR      : int Unsynchronized.ref
   val astar_tac         : claset -> int -> tactic
   val slow_astar_tac    : claset -> int -> tactic
   val best_tac          : claset -> int -> tactic
   val first_best_tac    : claset -> int -> tactic
   val slow_best_tac     : claset -> int -> tactic

   ObjectLogic.atomize_prems_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
 
 
 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
-val weight_ASTAR = ref 5;
+val weight_ASTAR = Unsynchronized.ref 5;
 
 fun astar_tac cs =
   ObjectLogic.atomize_prems_tac THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)