1.1 --- a/src/Provers/blast.ML Tue Feb 19 23:49:49 2002 +0100
1.2 +++ b/src/Provers/blast.ML Wed Feb 20 00:53:53 2002 +0100
1.3 @@ -415,12 +415,12 @@
1.4 (*A debugging function: replaces all Vars by dummy Frees for visual inspection
1.5 of whether they are distinct. Function revert undoes the assignments.*)
1.6 fun instVars t =
1.7 - let val name = ref "A"
1.8 + let val name = ref "a"
1.9 val updated = ref []
1.10 fun inst (TConst(a,t)) = inst t
1.11 | inst (Var(v as ref None)) = (updated := v :: (!updated);
1.12 v := Some (Free ("?" ^ !name));
1.13 - name := bump_string (!name))
1.14 + name := Symbol.bump_string (!name))
1.15 | inst (Abs(a,t)) = inst t
1.16 | inst (f $ u) = (inst f; inst u)
1.17 | inst _ = ()