src/HOL/UNITY/Project.thy

 apply (auto simp add: transient_def Domain_project_act)
 apply (subgoal_tac "act `` (C \<inter> extend_set h A) \<subseteq> - extend_set h A")
  prefer 2
  apply (simp add: stable_def constrains_def, blast) 
 (*back to main goal*)
-apply (erule_tac V = "?AA \<subseteq> -C \<union> ?BB" in thin_rl)
+apply (erule_tac V = "AA \<subseteq> -C \<union> BB" for AA BB in thin_rl)
 apply (drule bspec, assumption) 
 apply (simp add: extend_set_def project_act_def, blast)
 done
 
 (*converse might hold too?*)