diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Unix/Unix.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -618,7 +618,7 @@
   "root =xs\<Rightarrow> root' \<Longrightarrow> \<exists>att dir. root = Env att dir
     \<Longrightarrow> \<exists>att dir. root' = Env att dir"
 proof -
-  case antecedent
+  case rule_context
   with transition_type_safe show ?thesis
   proof (rule transitions_invariant)
     show "\<forall>x \<in> set xs. True" by blast
@@ -957,7 +957,7 @@
 lemma init_invariant: "init users =bogus\<Rightarrow> root \<Longrightarrow> invariant root bogus_path"
 proof -
   note eval = "setup" access_def init_def
-  case antecedent thus ?thesis
+  case rule_context thus ?thesis
     apply (unfold bogus_def bogus_path_def)
     apply (drule transitions_consD, rule transition.intros,
       (force simp add: eval)+, (simp add: eval)?)+
@@ -1126,7 +1126,7 @@
   \<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user1) \<and>
       can_exec root (xs @ [Rmdir user1 [user1, name1]]))"
 proof -
-  case antecedent
+  case rule_context
   with cannot_rmdir init_invariant preserve_invariant
   show ?thesis by (rule general_procedure)
 qed