diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt
index 84886bc2..3f3fb324 100644
--- a/forge/last-checker.rkt
+++ b/forge/last-checker.rkt
@@ -337,54 +337,6 @@
         [(Run? run) (infer-from-bounds)]
         [else (map list (primify run 'univ))]))
   
-;;   (define most-specific
-;;     (dfs-sigs run
-;;               (lambda (sig acc)
-;;                 ; We aren't going to look at the last-sterling-instance if we don't need to.
-;;                 ; Instead, look at the kodkod-bounds for this run.
-;;                 (define kodkod-bounds (if (Run? run) (Run-kodkod-bounds run) '()))
-;;                 ;(printf "inferring for ~a: visiting ~a; all kk bounds: ~a~n" atom sig kodkod-bounds)
-;;                 (define sig-kodkod-bounds-in-list
-;;                   (filter-map (lambda (b)
-;;                                 ;(printf "  considering bounded rel ~a vs target ~a~n" (bound-relation b) sig)
-;;                                 (if (equal? (bound-relation b) sig) (bound-upper b) #f))
-;;                               kodkod-bounds))
-;;                 ;(printf "  lst=~a~n" sig-kodkod-bounds-in-list)
-;;                 (cond
-;;                   ; Somehow this sig's kodkod bounds are empty; possibly not all sigs were used, or
-;;                   ; the run is still being created (i.e., called from send-to-kodkod)
-;;                   [(empty? sig-kodkod-bounds-in-list) (values acc #t)]
-;;                   [else 
-;;                    ; Is a tuple containing this atom's name a member of the upper bounds for this sig?
-;;                    (define new-acc (if (member (list (atom-name atom))
-;;                                                (first sig-kodkod-bounds-in-list))
-;;                                        (if (equal? acc '())
-;;                                            (list (Sig-name sig))
-;;                                            (cons (Sig-name sig) acc))
-;;                                        acc))
-;;                    (values new-acc #f)]))
-;;               (get-top-level-sigs run)
-;;               '()))
-;;   (when (> (get-verbosity) VERBOSITY_LOW) 
-;;     (printf "done inferring type for ~a; got sigs/remainders: ~a~n" atom most-specific))
-;;   ; Since we want most specific types, we cannot use primify directly. Instead, if a sig has
-;;   ; children (and is not abstract) just add its _remainder. Otherwise, if a sig has no children,
-;;   ; add it by name. Wrap each symbol in a list to denote a 1-arity tuple.
-;;   (if (empty? most-specific)
-;;       (map list (primify run 'univ))
-;;       (map list (filter-map (lambda (x)
-;;                               (define s (get-sig run x))
-;;                               (cond
-;;                                 ; Abstract sigs shouldn't be included
-;;                                 [(Sig-abstract s) #f]
-;;                                 ; if there is no child sig, this sig is included
-;;                                 [(empty? (get-children run s)) x]
-;;                                 ; if this sig has no children that are in the most-specific set
-;;                                 [(set-empty? (set-intersect (list->set (map Sig-name (get-children run s)))
-;;                                                             (list->set most-specific)))
-;;                                  (string->symbol (string-append (symbol->string x) "_remainder"))]
-;;                                 [else #f]))
-;         most-specific)))) 
   
 ; Runs a DFS over the sigs tree, starting from sigs in <sigs>.
 ; On each visited sig, <func> is called to obtain a new accumulated value