--- a/thys/Simplifying.thy	Tue May 24 15:13:41 2016 +0100
+++ b/thys/Simplifying.thy	Fri Jun 03 11:07:10 2016 +0100
@@ -75,7 +75,6 @@
 
 lemma L_fst_simp:
   shows "L(r) = L(fst (simp r))"
-using assms
 by (induct r) (auto)
 
 lemma Posix_simp: