1.1 --- a/src/Provers/blast.ML	Sun Jul 22 17:53:55 2007 +0200
     1.2 +++ b/src/Provers/blast.ML	Sun Jul 22 21:20:53 2007 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4    val ccontr            : thm
     1.5    val contr_tac         : int -> tactic
     1.6    val dup_intr          : thm -> thm
     1.7 -  val hyp_subst_tac     : bool ref -> int -> tactic
     1.8 +  val hyp_subst_tac     : bool -> int -> tactic
     1.9    val claset            : unit -> claset
    1.10    val rep_cs    : (* dependent on classical.ML *)
    1.11        claset -> {safeIs: thm list, safeEs: thm list,
    1.12 @@ -1015,7 +1015,7 @@
    1.13            in tracing sign brs0;
    1.14               if lim<0 then (traceMsg "Limit reached.  "; backtrack choices)
    1.15               else
    1.16 -             prv (Data.hyp_subst_tac trace :: tacs,
    1.17 +             prv (Data.hyp_subst_tac (!trace) :: tacs,
    1.18                    brs0::trs,  choices,
    1.19                    equalSubst sign
    1.20                      (G, {pairs = (br,haz)::pairs,

     2.1 --- a/src/Provers/hypsubst.ML	Sun Jul 22 17:53:55 2007 +0200
     2.2 +++ b/src/Provers/hypsubst.ML	Sun Jul 22 21:20:53 2007 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4  
     2.5  Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
     2.6  \                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
     2.7 -by (blast_hyp_subst_tac (ref true) 1);
     2.8 +by (blast_hyp_subst_tac true 1);
     2.9  *)
    2.10  
    2.11  signature HYPSUBST_DATA =
    2.12 @@ -49,7 +49,7 @@
    2.13  sig
    2.14    val bound_hyp_subst_tac    : int -> tactic
    2.15    val hyp_subst_tac          : int -> tactic
    2.16 -  val blast_hyp_subst_tac    : bool ref -> int -> tactic
    2.17 +  val blast_hyp_subst_tac    : bool -> int -> tactic
    2.18    val stac                   : thm -> int -> tactic
    2.19    val hypsubst_setup         : theory -> theory
    2.20  end;
    2.21 @@ -206,7 +206,7 @@
    2.22            val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
    2.23            val n = length hyps
    2.24        in
    2.25 -         if !trace then tracing "Substituting an equality" else ();
    2.26 +         if trace then tracing "Substituting an equality" else ();
    2.27           DETERM
    2.28             (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
    2.29                     rotate_tac 1 i,