src/HOL/UNITY/Constrains.thy

--- a/src/HOL/UNITY/Constrains.thy	Sun May 20 22:04:17 2018 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Sun May 20 22:04:46 2018 +0200
@@ -387,7 +387,7 @@
 
 (*Delete the nearest invariance assumption (which will be the second one
   used by Always_Int_I) *)
-lemmas Always_thin = thin_rl [of "F \<in> Always A"]
+lemmas Always_thin = thin_rl [of "F \<in> Always A"] for F A
 
 
 subsection\<open>Totalize\<close>