tuned -- more total;

--- a/src/Pure/Isar/rule_cases.ML	Wed Aug 20 11:51:39 2014 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Wed Aug 20 11:54:17 2014 +0200
@@ -330,7 +330,9 @@
 
 fun get_case_concl name (a, b) =
   if a = case_concl_tagN then
-    (case explode_args b of c :: cs => if c = name then SOME cs else NONE)
+    (case explode_args b of
+      c :: cs => if c = name then SOME cs else NONE
+    | [] => NONE)
   else NONE;
 
 fun add_case_concl (name, cs) = Thm.map_tags (fn tags =>