anchor.diff:  
   
   (defun clir->mlw (form)
  +  "Transforms a single CLIR FORM (toplevel or not) into its equivalent
  +WhyML representation."
     (typecase form
       (symbol (format nil "~(~A~)" form))
       (cons (case (car form)
  
positive.code:             parsed-forms)))
  
  (defun clir-file->mlw (form-list &key current-vu passed-forms stream)
    (if form-list
        (let ((form (first form-list)))
          (case (car form)
  
negative.code:           import-list))
  
  (defun generate-module (verification-unit parsed-forms &key stream)
    "Generates a WhyML module from a VERIFICATION-UNIT and a list of
  PARSED-FORMS, outputing the result in STREAM."
    (let ((theory-name (first verification-unit))
          (imports (imports->mlw '("int.Int"
                                   "ref.Ref"
  