rule_context: numbered cases;

--- a/src/Pure/Isar/auto_bind.ML	Thu Dec 22 00:29:01 2005 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Thu Dec 22 00:29:03 2005 +0100
@@ -36,8 +36,8 @@
 fun goal thy [prop] = statement_binds thy thesisN prop
   | goal _ _ = [((thesisN, 0), NONE)];
 
-fun cases thy [prop] = [RuleCases.simple true (thy, prop) rule_contextN]
-  | cases _ _ = [(rule_contextN, NONE)];
+fun cases _ [] = [(rule_contextN, NONE)]
+  | cases thy props = RuleCases.simple (thy, Logic.mk_conjunction_list props) rule_contextN;
 
 
 (* facts *)