# HG changeset patch
# User wenzelm
# Date 1136633189 -3600
# Node ID b971e113dee7e2e0566ce5a8b2b4ae2c3f8624af
# Parent  4000f368dc7f49b113a3d5004acd9ec11c059d07
RuleCases.make_simple;

diff -r 4000f368dc7f -r b971e113dee7 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Sat Jan 07 12:26:28 2006 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Sat Jan 07 12:26:29 2006 +0100
@@ -36,8 +36,8 @@
 fun goal thy [prop] = statement_binds thy thesisN prop
   | goal _ _ = [((thesisN, 0), NONE)];
 
-fun cases _ [] = [(rule_contextN, NONE)]
-  | cases thy props = RuleCases.simple (thy, Logic.mk_conjunction_list props) rule_contextN;
+fun cases thy [prop] = RuleCases.make_simple true (thy, prop) rule_contextN
+  | cases _ _ = [(rule_contextN, NONE)];
 
 
 (* facts *)