more explicit exception pattern (NB: unqualified exceptions without arguments are in danger of becoming catch-all patterns by accident);

--- a/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 16 17:13:38 2013 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 16 17:18:56 2013 +0200
@@ -35,7 +35,7 @@
            Pretty.fbrk, Syntax.pretty_term ctxt prop]));
       val ((f,_),_) = Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
               handle TERM _ => err ();
-      val info = Function.get_info ctxt f handle Empty => err ();
+      val info = Function.get_info ctxt f handle List.Empty => err ();
       val {elims, pelims, is_partial, ...} = info;
       val elims = if is_partial then pelims else the elims
       val cprop = cterm_of thy prop;