soegaard's answer is correct - this is the traditional expansion. However, drscheme is smart!
The following code I've found to be equivalent in running time:
Original source:
(define ((substitute lv value) e)
(cond [(LogicVar? e)
(type-case LogicVar e
[lv-any (id) (if (symbol=? id (lv-any-id lv))
value
e)]
[lv-cons (f r)
(lv-cons ((substitute lv value) f)
((substitute lv value) r))])]
[(cons? e)
(cons ((substitute lv value) (car e))
((substitute lv value) (cdr e)))]
[else e]))
Attempt at optimization:
(define (substitute lv value)
(local ([define inner
(lambda (e)
(cond [(LogicVar? e)
(type-case LogicVar e
[lv-any (id) (if (symbol=? id (lv-any-id lv))
value
e)]
[lv-cons (f r)
(lv-cons (inner f)
(inner r))])]
[(cons? e)
(cons (inner (car e))
(inner (cdr e)))]
[else e]))])
inner))
Code which heavily uses this function (multiple times, not just once) runs at 1800 ms for both versions. More interestingly, this version (my visualization of what was happening):
(define (substitute lv value)
(local ([define inner
(lambda (e)
(cond [(LogicVar? e)
(type-case LogicVar e
[lv-any (id) (if (symbol=? id (lv-any-id lv))
value
e)]
[lv-cons (f r)
(lv-cons ((substitute lv value) f)
((substitute lv value) r))])]
[(cons? e)
(cons ((substitute lv value) (car e))
((substitute lv value) (cdr e)))]
[else e]))])
inner))
Runs at 2000 ms. So there is definitely a slow-down if the calls to substitute within substitute were each creating a lambda, but it appears this is not the case with the shortcut notation.