1.1 --- a/src/Provers/classical.ML	Fri May 13 15:47:54 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri May 13 15:55:32 2011 +0200
     1.3 @@ -78,7 +78,6 @@
     1.4  
     1.5    val fast_tac: claset -> int -> tactic
     1.6    val slow_tac: claset -> int -> tactic
     1.7 -  val weight_ASTAR: int Unsynchronized.ref
     1.8    val astar_tac: claset -> int -> tactic
     1.9    val slow_astar_tac: claset -> int -> tactic
    1.10    val best_tac: claset -> int -> tactic
    1.11 @@ -711,6 +710,7 @@
    1.12  fun slow_step_tac cs i =
    1.13    safe_tac cs ORELSE appWrappers cs (inst_step_tac cs APPEND' haz_step_tac cs) i;
    1.14  
    1.15 +
    1.16  (**** The following tactics all fail unless they solve one goal ****)
    1.17  
    1.18  (*Dumb but fast*)
    1.19 @@ -737,18 +737,19 @@
    1.20  
    1.21  
    1.22  (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
    1.23 -val weight_ASTAR = Unsynchronized.ref 5;  (* FIXME argument / config option !? *)
    1.24 +
    1.25 +val weight_ASTAR = 5;
    1.26  
    1.27  fun astar_tac cs =
    1.28    Object_Logic.atomize_prems_tac THEN'
    1.29    SELECT_GOAL
    1.30 -    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + ! weight_ASTAR * lev)
    1.31 +    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
    1.32        (step_tac cs 1));
    1.33  
    1.34  fun slow_astar_tac cs =
    1.35    Object_Logic.atomize_prems_tac THEN'
    1.36    SELECT_GOAL
    1.37 -    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + ! weight_ASTAR * lev)
    1.38 +    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
    1.39        (slow_step_tac cs 1));
    1.40  
    1.41