2 files changed, 6 insertions, 6 deletions
diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy
index b73af758..4f80eade 100644
--- a/Test/dafny0/AdvancedLHS.dfy
+++ b/Test/dafny0/AdvancedLHS.dfy
@@ -8,7 +8,7 @@ class C {
     x := new C;
     x := new C.Init();
     havoc x;
-    x := choose(S);
+    x := choose S;
 
     // test evaluation order
     var c := x;
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 25e6cc5c..74512e01 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -22,20 +22,20 @@ method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r:
   ensures r == c;
 {
   var Q := people;
-  var x := choose(Q);
+  var x := choose Q;
   while (Q != {x})
     //invariant Q <= people;  // inv1 in Rodin's Celebrity_1, but it's not needed here
     invariant IsCelebrity(c, Q);  // inv2
     invariant x in Q;
     decreases Q;
   {
-    var y := choose(Q - {x});
+    var y := choose Q - {x};
     if (Knows(x, y)) {
       Q := Q - {x};  // remove_1
     } else {
       Q := Q - {y};  assert x in Q;  // remove_2
     }
-    x := choose(Q);
+    x := choose Q;
   }
   r := x;
 }
@@ -44,7 +44,7 @@ method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r:
   requires IsCelebrity(c, people);
   ensures r == c;
 {
-  var b := choose(people);
+  var b := choose people;
   var R := people - {b};
   while (R != {})
     invariant R <= people;  // inv1
@@ -54,7 +54,7 @@ method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r:
 
     decreases R;
   {
-    var x := choose(R);
+    var x := choose R;
     if (Knows(x, b)) {
       R := R - {x};
     } else {