src/HOL/HOLCF/IOA/meta_theory/Automata.thy

 
 lemma is_asig_of_rename: "is_asig_of A ==> is_asig_of (rename A f)"
 apply (simp add: is_asig_of_def rename_def rename_set_def asig_internals_def
   asig_outputs_def asig_inputs_def actions_def is_asig_def asig_of_def)
 apply auto
-apply (drule_tac [!] s = "Some ?x" in sym)
+apply (drule_tac [!] s = "Some _" in sym)
 apply auto
 done
 
 lemmas [simp] = is_asig_of_par is_asig_of_restrict
   is_asig_of_rename is_trans_of_par is_trans_of_restrict is_trans_of_rename