| changeset 12346 | e7b1956f4eae |
| parent 11783 | aee100a086b1 |
| child 12371 | 80ca9058db95 |
--- a/src/Provers/blast.ML Mon Dec 03 21:01:11 2001 +0100 +++ b/src/Provers/blast.ML Mon Dec 03 21:01:37 2001 +0100 @@ -1186,9 +1186,7 @@ lim = lim} :: brs) end | prv (tacs, trs, choices, _ :: brs) = backtrack choices - in init_gensym(); - prv ([], [], [(!ntrail, length brs, PROVE)], brs) - end; + in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end; (*Construct an initial branch.*)