src/ZF/UNITY/Constrains.thy

 lemma Always_Diff_Un_eq: "[| F \<in> Always(A) |] ==> (F \<in> Always(C-A \<union> B)) \<longleftrightarrow> (F \<in> Always(B))"
 by (auto simp add: Always_eq_includes_reachable)
 
 (*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
 
 (*To allow expansion of the program's definition when appropriate*)
 named_theorems program "program definitions"
 
 ML