Modular ACL2 reacts poorly to mixing of "code" and exports

[pnkfelix]

Open up the following in Modular ACL2, select the module m, and click "Admit All" button

(interface Ig (sig g (y)))
(interface Ih (sig h (z)))

(module m 
  (defun g (y) (+ y y))
  (defun h (z) (g z))
  (export Ig)
  (in-theory (disable (:executable-counterpart h)))
  (export Ih))

I get the following internal error from the guts of Dracula/DrScheme:

highlight/save: start position 177 > end position 125

 === context ===
/Users/pnkfelix/Library/PLT Scheme/planet/300/4.1.5/cache/cce/dracula.plt/8/2/drscheme/dracula-drscheme-tab.ss:

The obvious workaround is to put the in-theory invocation above the export. Note however that I think some people might have reason to write down in-theory invocations that effect the proof attempts for some signatures but not all of them.

In any case the internal error is bad.