1 files changed, 12 insertions, 12 deletions
diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy
index a853b82c..6b8f1377 100644
--- a/Test/hofs/TreeMapSimple.dfy
+++ b/Test/hofs/TreeMapSimple.dfy
@@ -6,7 +6,7 @@ datatype List<A> = Nil | Cons(head: A,tail: List<A>)
 datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>)
 
 function ListData(xs : List) : set
-  ensures forall x :: x in ListData(xs) ==> x < xs;
+  ensures forall x :: x in ListData(xs) ==> x < xs
 {
   match xs
     case Nil => {}
@@ -14,32 +14,32 @@ function ListData(xs : List) : set
 }
 
 function TreeData(t0 : Tree) : set
-  ensures forall t :: t in TreeData(t0) ==> t < t0;
+  ensures forall t :: t in TreeData(t0) ==> t < t0
 {
   var Branch(x,ts) := t0;
   {x} + set t, y | t in ListData(ts) && y in TreeData(t) :: y
 }
 
-function Pre(f : A -> B, s : set<A>) : bool
-  reads (set x, y | x in s && y in f.reads(x) :: y);
+function Pre<A,B>(f : A -> B, s : set<A>) : bool
+  reads (set x, y | x in s && y in f.reads(x) :: y)
 {
   forall x :: x in s ==> f.reads(x) == {} && f.requires(x)
 }
 
-function method Map(xs : List<A>, f : A -> B): List<B>
-  reads Pre.reads(f, ListData(xs));
-  requires Pre(f, ListData(xs));
-  decreases xs;
+function method Map<A,B>(xs : List<A>, f : A -> B): List<B>
+  reads Pre.reads(f, ListData(xs))
+  requires Pre(f, ListData(xs))
+  decreases xs
 {
   match xs
     case Nil => Nil
     case Cons(x,xs) => Cons(f(x),Map(xs,f))
 }
 
-function method TMap(t0 : Tree<A>, f : A -> B) : Tree<B>
-  reads Pre.reads(f, TreeData(t0));
-  requires Pre(f, TreeData(t0));
-  decreases t0;
+function method TMap<A,B>(t0 : Tree<A>, f : A -> B) : Tree<B>
+  reads Pre.reads(f, TreeData(t0))
+  requires Pre(f, TreeData(t0))
+  decreases t0
 {
   var Branch(x,ts) := t0;
   Branch(f(x),Map(ts, t  requires t in ListData(ts)