--- a/thys/Lexer.thy	Tue May 24 15:13:41 2016 +0100
+++ b/thys/Lexer.thy	Fri Jun 03 11:07:10 2016 +0100
@@ -620,7 +620,6 @@
 
 lemma lexer_correct_None:
   shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"
-using assms
 apply(induct s arbitrary: r)
 apply(simp add: nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
@@ -629,7 +628,6 @@
 
 lemma lexer_correct_Some:
   shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
-using assms
 apply(induct s arbitrary: r)
 apply(auto simp add: Posix_mkeps nullable_correctness)[1]
 apply(drule_tac x="der a r" in meta_spec)