diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Bali/AxSem.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -687,7 +687,7 @@
 done
 
 lemma weaken: 
- "G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
+ "G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> \<forall>ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
 apply (erule ax_derivs.induct)
 (*42 subgoals*)
 apply       (tactic "ALLGOALS (strip_tac @{context})")