--- a/thys/Re1.thy	Thu Feb 12 14:00:45 2015 +0000
+++ b/thys/Re1.thy	Sat Feb 14 08:35:21 2015 +0000
@@ -321,7 +321,7 @@
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply (metis ValOrd.intros)
-apply(simp add: POSIX_def)
+apply(simp)
 apply(auto)[1]
 apply(simp add: POSIX_def)
 apply(auto)[1]