--- 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
--- 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 *)
--- 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