--- a/src/HOL/Bali/DefiniteAssignment.thy Thu Apr 21 22:00:28 2005 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Thu Apr 21 22:02:06 2005 +0200
@@ -1346,7 +1346,7 @@
subseteq_B_B': "B \<subseteq> B'"
shows "\<exists> A'. Env \<turnstile> B' \<guillemotright>t\<guillemotright> A'"
proof -
- note assigned.select_convs [CPure.intro]
+ note assigned.select_convs [Pure.intro]
from da
show "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
proof (induct)