diff -r 0028bd06a19c -r e7265e70fd7c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 04 21:10:57 2001 +0200
@@ -580,7 +580,7 @@
 
 (* setup goals *)
 
-val antN = "antecedent";
+val rule_contextN = "rule_context";
 
 fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
   let
@@ -604,7 +604,7 @@
       commas (map (Sign.string_of_term (sign_of state)) vars));
     state'
     |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds))
-    |> map_context (ProofContext.add_cases (RuleCases.make true goal [antN]))
+    |> map_context (ProofContext.add_cases (RuleCases.make true goal [rule_contextN]))
     |> auto_bind_goal prop
     |> (if is_chain state then use_facts else reset_facts)
     |> new_block