# HG changeset patch
# User blanchet
# Date 1412088003 -7200
# Node ID fb6508a73261b93b8de05fb9030cc3adb208e2d3
# Parent  430306aa03b14c2b5b99920cf98f9e15d6b2fdef
don't call 'hd' on a possibly empty list

diff -r 430306aa03b1 -r fb6508a73261 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Sep 30 16:01:46 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Sep 30 16:40:03 2014 +0200
@@ -77,7 +77,8 @@
       val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
       val goal_t = Logic.list_implies (map prop_of chained @ hyp_ts, concl_t)
 
-      fun try_methss ress [] =
+      fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
+        | try_methss ress [] =
           (used_facts,
            (case AList.lookup (op =) ress preferred_meth of
              SOME play => (preferred_meth, play)