diff -r fe92356ade42 -r bcf4828bb125 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Jun 02 16:49:44 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Jun 02 17:05:40 2016 +0200
@@ -214,7 +214,7 @@
   let val thy = Proof_Context.theory_of ctxt
   in Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty) end;
 
-fun unfold_thms ctxt thms = Local_Defs.unfold0 ctxt (distinct Thm.eq_thm_prop thms);
+val unfold_thms = Local_Defs.unfold0;
 
 fun name_noted_thms _ _ [] = []
   | name_noted_thms qualifier base ((local_name, thms) :: noted) =