# HG changeset patch
# User wenzelm
# Date 1408528457 -7200
# Node ID 47ecbef7274bd4f79957561e810f078ae9f731e2
# Parent  14c8269d0de9acff78a9a045d6282917ceb51397
tuned -- more total;

diff -r 14c8269d0de9 -r 47ecbef7274b src/Pure/Isar/rule_cases.ML
--- 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 =>