diff -r c80a08ff2a85 -r 420e03a2d9cc Test.thy
--- a/Test.thy	Mon Mar 21 14:41:40 2016 +0000
+++ b/Test.thy	Mon Mar 21 15:06:52 2016 +0000
@@ -285,7 +285,7 @@
   shows "single_valuedP (waits2 s)"
 using assms
 unfolding single_valued_def
-by (metis Collect_splitD fst_eqD sndI waits2_unique)
+by (simp add: Product_Type.Collect_case_prodD waits2_unique)
 
 lemma single_valued_holds2:
   assumes "vt s"