# HG changeset patch
# User berghofe
# Date 1184147643 -7200
# Node ID 60b7800338d5415d5f7eb979c86e5808ad9e77ab
# Parent  2215169c93fa867477e895bd90b5ed7fa64065aa
Renamed accessible part for predicates to accp.

diff -r 2215169c93fa -r 60b7800338d5 src/HOL/ex/Unification.thy
--- 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`)