(* Code fragment for elaborating fun bindings.
   Expects Variable, ILModule, and LL to be open.
*)
| EL.Dfun (fid, argid, dom, cod, t) =>
     let 
        val dom' = ElaborateType.elabTp ctx dom
        val cod' = ElaborateType.elabTp ctx cod
        val vcself = newvar ()
        val c = Crec (vcself, Carrow (Cvar vcself, Carrow (dom', cod')))

        val vself = newvar ()
        val varg = newvar ()
        val vc = newvar ()
        val vm = newvar ()
        val ctx' = 
           (ANON, vc, vm, Smod [(VAL fid, newvar (), Sval (Carrow (dom', cod'))),
                                (VAL argid, newvar (), Sval dom')])
           ::
           ctx

        val (cod'', t') = elabTerm ctx' t

        val () = EquivModule.equiv (#1 (stripctx ctx')) cod' cod'' Ktype

        val m =
           Mval 
           (Tlet (vself,
                  Troll (Tlam (vself, c,
                               Tlam (varg, dom',
                                     Tletm (vc, vm,
                                            Mstruct [(newvar (), newvar (), Mval (Tapp (Tunroll (Tvar vself),
                                                                                        Tvar vself))),
                                                     (newvar (), newvar (), Mval (Tvar varg))],
                                            t',
                                            cod'))),
                         c),
                  Tapp (Tunroll (Tvar vself), Tvar vself)))
     in
        (Smod [(VAL fid, newvar (), Sval (Carrow (dom', cod')))],
         Mstruct [(newvar (), newvar (), m)])
     end