--- old-mainline/divine/toolkit/list.h  2014-01-24 20:56:57.305866248 +0100
+++ new-mainline/divine/toolkit/list.h  2014-01-24 20:56:57.307866288 +0100
@@ -17,7 +17,9 @@ template< int N > struct ConsAt;
 template<>
 struct ConsAt< 0 > {
     template< typename Cons >
-    static constexpr auto get( Cons &c ) -> decltype( c.car ) {
+    using T = typename Cons::Car;
+    template< typename Cons >
+    static constexpr T< Cons > get( Cons &c ) {
         return c.car;
     }
 };
@@ -25,7 +27,9 @@ struct ConsAt< 0 > {
 template< int N >
 struct ConsAt {
     template< typename Cons >
-    static constexpr auto get( Cons &c ) -> decltype( ConsAt< N - 1 >::get( c.cdr ) )
+    using T = typename ConsAt< N - 1 >::template T< typename Cons::Cdr >;
+    template< typename Cons >
+    static constexpr T< Cons > get( Cons &c )
     {
         return ConsAt< N - 1 >::get( c.cdr );
     }
@@ -84,7 +88,7 @@ constexpr auto concat( L1 l1, L2 l2 ) ->
 }

 template< int I, typename Cons >
-auto decons( Cons c ) -> decltype( ConsAt< I >::get( c ) )
+auto decons( Cons c ) -> typename list::ConsAt< I >::template T< Cons > &
 {
     return c.template get< I >();
 }

--- old-mainline/divine/llvm/execution.h    2014-01-24 20:56:57.306866268 +0100
+++ new-mainline/divine/llvm/execution.h    2014-01-24 20:56:57.307866288 +0100
@@ -69,7 +69,7 @@ template< typename X >
 struct UnPtr< X * > { typedef X T; };

 template< int I, typename Cons >
-auto deconsptr( Cons c ) -> typename UnPtr< decltype( list::ConsAt< I >::get( c ) ) >::T &
+auto deconsptr( Cons c ) -> typename UnPtr< typename list::ConsAt< I >::template T< Cons > >::T &
 {
     return *c.template get< I >();
 }