From d30478027bb51b9507a31538799ca285df096bf9 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 26 Mar 2011 04:06:37 +0000
Subject: Dafny: improved and corrected physical/ghost distinction

---
 Test/dafny1/Celebrity.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Test/dafny1/Celebrity.dfy')

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index eed06bb1..77af9327 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -4,7 +4,7 @@ method Pick<T>(S: set<T>) returns (t: T);
   requires S != {};
   ensures t in S;
 
-static function Knows<Person>(a: Person, b: Person): bool;
+static function method Knows<Person>(a: Person, b: Person): bool;
   requires a != b;  // forbid asking about the reflexive case
 
 static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
-- 
cgit v1.2.3