src/Provers/blast.ML
changeset 12902 a23dc0b7566f
parent 12403 3e3bd3d449b5
child 13550 5a176b8dda84
     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 _             = ()