# HG changeset patch
# User wenzelm
# Date 1305294932 -7200
# Node ID 36f787ae5f705bca21f2bd59ba11f50688e4098a
# Parent  e07e56300faaf5988017c73182ee3d338dfaf846
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);

diff -r e07e56300faa -r 36f787ae5f70 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri May 13 15:47:54 2011 +0200
+++ b/src/Provers/classical.ML	Fri May 13 15:55:32 2011 +0200
@@ -78,7 +78,6 @@
 
   val fast_tac: claset -> int -> tactic
   val slow_tac: claset -> int -> tactic
-  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
@@ -711,6 +710,7 @@
 fun slow_step_tac cs i =
   safe_tac cs ORELSE appWrappers cs (inst_step_tac cs APPEND' haz_step_tac cs) i;
 
+
 (**** The following tactics all fail unless they solve one goal ****)
 
 (*Dumb but fast*)
@@ -737,18 +737,19 @@
 
 
 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
-val weight_ASTAR = Unsynchronized.ref 5;  (* FIXME argument / config option !? *)
+
+val weight_ASTAR = 5;
 
 fun astar_tac cs =
   Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL
-    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + ! weight_ASTAR * lev)
+    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
       (step_tac cs 1));
 
 fun slow_astar_tac cs =
   Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL
-    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + ! weight_ASTAR * lev)
+    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
       (slow_step_tac cs 1));