# HG changeset patch
# User wenzelm
# Date 1210967607 -7200
# Node ID c795d4b706b1a3bc6fcb5013b671762c8e92c9b3
# Parent  5d9f78c3d6de3fe23b4c102c801507e219650b3c
removed obsolete case rule_context;

diff -r 5d9f78c3d6de -r c795d4b706b1 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Fri May 16 21:41:07 2008 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Fri May 16 21:53:27 2008 +0200
@@ -336,8 +336,7 @@
 
   Any goal statement causes some term abbreviations (such as
   @{variable_ref "?thesis"}) to be bound automatically, see also
-  \secref{sec:term-abbrev}.  Furthermore, the local context of a
-  (non-atomic) goal is provided via the @{case_ref rule_context} case.
+  \secref{sec:term-abbrev}.
 
   The optional case names of @{element_ref "obtains"} have a twofold
   meaning: (1) during the of this claim they refer to the the local
diff -r 5d9f78c3d6de -r c795d4b706b1 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Fri May 16 21:41:07 2008 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Fri May 16 21:53:27 2008 +0200
@@ -7,12 +7,10 @@
 
 signature AUTO_BIND =
 sig
-  val rule_contextN: string
   val thesisN: string
   val thisN: string
   val assmsN: string
   val goal: theory -> term list -> (indexname * term option) list
-  val cases: theory -> term list -> (string * RuleCases.T option) list
   val facts: theory -> term list -> (indexname * term option) list
   val no_facts: (indexname * term option) list
 end;
@@ -22,7 +20,6 @@
 
 (** bindings **)
 
-val rule_contextN = "rule_context";
 val thesisN = "thesis";
 val thisN = "this";
 val assmsN = "assms";
@@ -38,9 +35,6 @@
 fun goal thy [prop] = statement_binds thy thesisN prop
   | goal _ _ = [((thesisN, 0), NONE)];
 
-fun cases thy [prop] = RuleCases.make_simple true (thy, prop) rule_contextN
-  | cases _ _ = [(rule_contextN, NONE)];
-
 
 (* facts *)
 
diff -r 5d9f78c3d6de -r c795d4b706b1 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri May 16 21:41:07 2008 +0200
+++ b/src/Pure/Isar/proof.ML	Fri May 16 21:53:27 2008 +0200
@@ -808,7 +808,6 @@
     goal_state
     |> map_context (init_context #> Variable.set_body true)
     |> put_goal (SOME (make_goal (((kind, pos), propss'), [], [], goal, before_qed, after_qed')))
-    |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
     |> map_context (ProofContext.auto_bind_goal props)
     |> chaining ? (`the_facts #-> using_facts)
     |> put_facts NONE