Renamed accessible part for predicates to accp.

--- a/src/HOL/ex/Unification.thy	Wed Jul 11 11:52:45 2007 +0200
+++ b/src/HOL/ex/Unification.thy	Wed Jul 11 11:54:03 2007 +0200
@@ -458,7 +458,7 @@
 
   from `unify_dom (M \<cdot> N, M' \<cdot> N')`
   have "unify_dom (M, M')"
-    by (rule acc_downward) (rule unify_rel.intros)
+    by (rule accp_downward) (rule unify_rel.intros)
   hence no_new_vars: 
     "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
     by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)