1 files changed, 9 insertions, 9 deletions
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index 41adcf50..2b5187a4 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype List<X> = Nil | Cons(Node<X>, List<X>)
@@ -42,13 +42,13 @@ function ToSeq<X>(list: List<X>): seq<X>
     case Nary(nn) => ToSeq(nn) + ToSeq(rest)
 }
 
-ghost method Theorem<X>(list: List<X>)
+lemma Theorem<X>(list: List<X>)
   ensures ToSeq(list) == ToSeq(FlattenMain(list));
 {
   Lemma(list, Nil);
 }
 
-ghost method Lemma<X>(list: List<X>, ext: List<X>)
+lemma Lemma<X>(list: List<X>, ext: List<X>)
   requires IsFlat(ext);
   ensures ToSeq(list) + ToSeq(ext) == ToSeq(Flatten(list, ext));
 {
@@ -73,27 +73,27 @@ function NegFac(n: int): int
   if -1 <= n then -1 else - NegFac(n+1) * n
 }
 
-ghost method LemmaAll()
+lemma LemmaAll()
   ensures forall n :: NegFac(n) <= -1;  // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
 {
 }
 
-ghost method LemmaOne(n: int)
+lemma LemmaOne(n: int)
   ensures NegFac(n) <= -1;  // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
 {
 }
 
-ghost method LemmaAll_Neg()
-  ensures forall n :: NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger
+lemma LemmaAll_Neg() //FIXME I don't understand the comment below; what trigger?
+  ensures forall n {:nowarn} :: NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger
 {
 }
 
-ghost method LemmaOne_Neg(n: int)
+lemma LemmaOne_Neg(n: int) //FIXME What trigger?
   ensures NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger
 {
 }
 
-ghost method LemmaOneWithDecreases(n: int)
+lemma LemmaOneWithDecreases(n: int)
   ensures NegFac(n) <= -1;  // here, the programmer gives a good well-founded order, so this verifies
   decreases -n;
 {