--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Nov 10 21:49:48 2014 +0100
@@ -2471,7 +2471,7 @@
fun distinct_prems ctxt thm =
Goal.prove (*no sorry*) ctxt [] []
(thm |> Thm.prop_of |> Logic.strip_horn |>> distinct (op aconv) |> Logic.list_implies)
- (fn _ => HEADGOAL (cut_tac thm THEN' atac) THEN ALLGOALS eq_assume_tac);
+ (fn _ => HEADGOAL (cut_tac thm THEN' assume_tac ctxt) THEN ALLGOALS eq_assume_tac);
fun eq_ifIN _ [thm] = thm
| eq_ifIN ctxt (thm :: thms) =