diff --git a/Induction/Structural/Types.hs b/Induction/Structural/Types.hs
--- a/Induction/Structural/Types.hs
+++ b/Induction/Structural/Types.hs
@@ -148,6 +148,8 @@
 -- | Obligations with tagged variables (see `Tagged` and `unTag`)
 type TaggedObligation c v t = Obligation c (Tagged v) t
 
+return []
+
 -- | Tri-traverse of Obligation
 trObligation :: Applicative f => (c -> f c') -> (v -> f v') -> (t -> f t') -> Obligation c v t -> f (Obligation c' v' t')
 trObligation = $(genTraverse ''Obligation)
diff --git a/structural-induction.cabal b/structural-induction.cabal
--- a/structural-induction.cabal
+++ b/structural-induction.cabal
@@ -1,6 +1,6 @@
 name:               structural-induction
 category:           Theorem Provers, Logic
-version:            0.1.1
+version:            0.1.2
 license:            LGPL-3
 license-file:       LICENSE
 author:             Dan Rosén
@@ -9,7 +9,7 @@
 bug-reports:        http://www.github.com/danr/structural-induction/issues
 build-type:         Simple
 cabal-version:      >= 1.8
-tested-with:        GHC == 7.4.1, GHC == 7.6.1
+tested-with:        GHC == 7.4.2, GHC == 7.6.3, GHC == 7.8.3
 synopsis:           Instantiate structural induction schemas for algebraic data types
 description:        See documentation for Induction.Structural
 
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -91,7 +91,7 @@
     forAllShrink (startFromTypes tys) (mapM shrinkRepr') $ \ start ->
         forAll (makeTracer start parts) $ \ trace ->
             case loop trace of
-                Just _  -> printTestCase (showOblig parts) False
+                Just _  -> counterexample (showOblig parts) False
                 Nothing -> property True
   where parts = ind sii tc