diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- 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) =