4 files changed, 8 insertions, 8 deletions
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 965f0787..7a443e47 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -109,8 +109,8 @@ module T refines S {
   }
 }
 module A {
-   import X as S default T
-   import Y as S default T
+   import X : T
+   import Y : T
    import Z = T
    method run() {
      var x := new X.C;
@@ -128,7 +128,7 @@ method NotMain() {
 
 
 abstract module S1 {
-  import B as S default T
+  import B : T
   method do()
 }
 
@@ -138,7 +138,7 @@ module T1 refines S1 {
   }
 }
 module A1 {
-   import X as S1 default T1
+   import X : T1
    method run() {
      X.do();
      var x := new X.B.C;
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 3ffa5a23..3025cc00 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -130,6 +130,6 @@ abstract module Regression {
 
   abstract module B
   {
-    import X as A
+    import X : A
   }
 }
diff --git a/Test/dafny0/Modules2.dfy b/Test/dafny0/Modules2.dfy
index a8dde8ce..beb80546 100644
--- a/Test/dafny0/Modules2.dfy
+++ b/Test/dafny0/Modules2.dfy
@@ -31,7 +31,7 @@ module Test {
 }
 
 module Test2 {
-  import opened B as A
+  import opened B : A
   method m() {
     var c := new C;   // fine, as A was opened
     var c' := new B.C;// also fine, as A is bound
diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy
index e1c0756c..b3cde309 100644
--- a/Test/dafny0/OpaqueFunctions.dfy
+++ b/Test/dafny0/OpaqueFunctions.dfy
@@ -44,7 +44,7 @@ module A' refines A {
 }
 
 module B {
-  import X as A
+  import X : A
   method Main() {
     var c := new X.C();
     c.M();  // fine
@@ -68,7 +68,7 @@ module B {
   }
 }
 module B_direct {
-  import X as A'
+  import X : A'
   method Main() {
     var c := new X.C();
     c.M();  // fine