diff -r 03c5f0393a2c -r f8b2bf858caf thys/Hoare_abc.thy
--- a/thys/Hoare_abc.thy	Tue Mar 25 11:20:36 2014 +0000
+++ b/thys/Hoare_abc.thy	Thu Mar 27 11:50:37 2014 +0000
@@ -343,8 +343,8 @@
   ultimately show ?case 
     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
     apply (unfold IA_def, intro condI, assumption+)
-    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
-    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
+    apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI)
+    apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI)
     apply (unfold fam_conj_disj_simp[OF fresh_atm])
     apply (auto simp:sep_conj_ac fam_conj_simps)
     (***************************************************************************)
@@ -527,8 +527,8 @@
   ultimately show ?case 
     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
     apply (unfold IA_def, intro condI, assumption+)
-    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
-    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
+    apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI)
+    apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI)
     apply (unfold fam_conj_disj_simp[OF fresh_atm])
     apply (auto simp:sep_conj_ac fam_conj_simps)
     (***************************************************************************)
@@ -712,8 +712,8 @@
   ultimately show ?case 
     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
     apply (unfold IA_def, intro condI, assumption+)
-    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
-    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
+    apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI)
+    apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI)
     apply (unfold fam_conj_disj_simp[OF fresh_atm])
     apply (auto simp:sep_conj_ac fam_conj_simps)
     (***************************************************************************)
@@ -912,8 +912,8 @@
   ultimately show ?case 
     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
     apply (unfold IA_def, intro condI, assumption+)
-    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
-    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
+    apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI)
+    apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI)
     apply (unfold fam_conj_disj_simp[OF fresh_atm])
     by (auto simp:sep_conj_ac fam_conj_simps)
 qed