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