--- 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,