# HG changeset patch
# User wenzelm
# Date 1185132053 -7200
# Node ID edca7f581c0977f2eff20b13aa93dd63424ca291
# Parent  cca404a6217377f8738f0888120a10aa72ee9a3d
blast_hyp_subst_tac: plain bool argument;

diff -r cca404a62173 -r edca7f581c09 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sun Jul 22 17:53:55 2007 +0200
+++ b/src/Provers/blast.ML	Sun Jul 22 21:20:53 2007 +0200
@@ -48,7 +48,7 @@
   val ccontr            : thm
   val contr_tac         : int -> tactic
   val dup_intr          : thm -> thm
-  val hyp_subst_tac     : bool ref -> int -> tactic
+  val hyp_subst_tac     : bool -> int -> tactic
   val claset            : unit -> claset
   val rep_cs    : (* dependent on classical.ML *)
       claset -> {safeIs: thm list, safeEs: thm list,
@@ -1015,7 +1015,7 @@
           in tracing sign brs0;
              if lim<0 then (traceMsg "Limit reached.  "; backtrack choices)
              else
-             prv (Data.hyp_subst_tac trace :: tacs,
+             prv (Data.hyp_subst_tac (!trace) :: tacs,
                   brs0::trs,  choices,
                   equalSubst sign
                     (G, {pairs = (br,haz)::pairs,
diff -r cca404a62173 -r edca7f581c09 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sun Jul 22 17:53:55 2007 +0200
+++ b/src/Provers/hypsubst.ML	Sun Jul 22 21:20:53 2007 +0200
@@ -28,7 +28,7 @@
 
 Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
 \                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
-by (blast_hyp_subst_tac (ref true) 1);
+by (blast_hyp_subst_tac true 1);
 *)
 
 signature HYPSUBST_DATA =
@@ -49,7 +49,7 @@
 sig
   val bound_hyp_subst_tac    : int -> tactic
   val hyp_subst_tac          : int -> tactic
-  val blast_hyp_subst_tac    : bool ref -> int -> tactic
+  val blast_hyp_subst_tac    : bool -> int -> tactic
   val stac                   : thm -> int -> tactic
   val hypsubst_setup         : theory -> theory
 end;
@@ -206,7 +206,7 @@
           val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
           val n = length hyps
       in
-         if !trace then tracing "Substituting an equality" else ();
+         if trace then tracing "Substituting an equality" else ();
          DETERM
            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
                    rotate_tac 1 i,