# HG changeset patch
# User wenzelm
# Date 1135207743 -3600
# Node ID 255eaf0a2119b0dd99f2773751636b24831195d3
# Parent  ca9a864018d6683c9e87ac4242820df6395fe931
rule_context: numbered cases;

diff -r ca9a864018d6 -r 255eaf0a2119 src/Pure/Isar/auto_bind.ML
--- 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 *)