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