# HG changeset patch
# User krauss
# Date 1283241606 -7200
# Node ID 39db63c45683238095b8edad1c4900d0226327e2
# Parent  fd6b9bdb428e81834ba067dcb1a0949f30ddab3d
more permissive: simplification solves the goal when rhs = undefined

diff -r fd6b9bdb428e -r 39db63c45683 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Mon Aug 30 18:32:40 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Tue Aug 31 10:00:06 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