diff --git a/src/examples/temp-queue1.broken.c b/src/examples/temp-queue1.broken.c
index 066e48d0..b6fb4203 100644
--- a/src/examples/temp-queue1.broken.c
+++ b/src/examples/temp-queue1.broken.c
@@ -1,5 +1,9 @@
 #include "list.h"
 
+
+/*@ function (datatype seq) rev(datatype seq xs) @*/
+
+
 // N.b.: This is wrong!
 /*@
 function [rec] (datatype seq) snoc(datatype seq xs, i32 y) {