# HG changeset patch
# User haftmann
# Date 1283269587 -7200
# Node ID 94d239bbb61851559e3e70f9ab87793254c2ab94
# Parent  39db63c45683238095b8edad1c4900d0226327e2# Parent  bd77e092f67c2592f644994e6c2785c832d19ca7
merged

diff -r bd77e092f67c -r 94d239bbb618 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Tue Aug 31 16:51:29 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Tue Aug 31 17:46:27 2010 +0200
@@ -860,9 +860,9 @@
           rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
           THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
           THEN (simp_default_tac (simpset_of ctxt) 1)
-          THEN (etac not_acc_down 1)
-          THEN ((etac R_cases)
-            THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
+          THEN TRY ((etac not_acc_down 1)
+            THEN ((etac R_cases)
+              THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1))
         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
       end
   in