--- 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