Partial fix for Issue 709.

frog/minfrog

Index: frog/minfrog
diff --git a/frog/minfrog b/frog/minfrog
index 92e229717f956e7753d3e1934ef3048fe396390b..3d720248031eb3a5a7cd2f04c70230a3808c5e8b 100755
--- a/frog/minfrog
+++ b/frog/minfrog
@@ -2329,7 +2329,7 @@ WorldGenerator.prototype._prototypeOf = function(type, name) {
   }
   else if (type.get$isHiddenNativeType()) {
     this.corejs.ensureDynamicProto();
-    return ('\$dynamic("' + name + '").' + type.get$jsname());
+    return ('\$dynamic("' + name + '").' + type.get$definition().get$nativeType().get$name());
   }
   else {
     return ('' + type.get$jsname() + '.prototype.' + name);
@@ -2370,7 +2370,12 @@ WorldGenerator.prototype.writeType = function(type) {
       this.writer.writeln(('function ' + type.get$jsname() + '() {}'));
     }
     else if (type.get$jsname() != nativeName) {
-      this.writer.writeln(('' + type.get$jsname() + ' = ' + nativeName + ';'));
+      if (type.get$isHiddenNativeType()) {
+        this.writer.writeln(('function ' + type.get$jsname() + '() {}'));
+      }
+      else {
+        this.writer.writeln(('' + type.get$jsname() + ' = ' + nativeName + ';'));
+      }
     }
   }
   if (!type.get$isTop()) {