From a79e9f5552c4292ffae87378ef7492f25023ff89 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 22 Aug 2024 08:04:01 -0700
Subject: [PATCH] Make SetToOrderedSequence compilable again

---
 StandardLibrary/src/StandardLibrary.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/StandardLibrary/src/StandardLibrary.dfy b/StandardLibrary/src/StandardLibrary.dfy
index 62f385333..2e0bfb568 100644
--- a/StandardLibrary/src/StandardLibrary.dfy
+++ b/StandardLibrary/src/StandardLibrary.dfy
@@ -335,7 +335,7 @@ module StandardLibrary {
    * The function is compilable, but will not exhibit enviable performance.
    */
 
-  function SetToOrderedSequence<T(!new,==)>(s: set<seq<T>>, less: (T, T) -> bool): (q: seq<seq<T>>)
+  function method {:tailrecursion} SetToOrderedSequence<T(!new,==)>(s: set<seq<T>>, less: (T, T) -> bool): (q: seq<seq<T>>)
     requires Trichotomous(less) && Transitive(less)
     ensures |s| == |q|
     ensures forall i :: 0 <= i < |q| ==> q[i] in s