--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Thu Jun 02 16:49:44 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Thu Jun 02 17:05:40 2016 +0200
@@ -47,8 +47,7 @@
fun select_prem_tac ctxt n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac ctxt thin_rl,
tac, REPEAT_DETERM_N (n - k) o etac ctxt thin_rl]);
-fun unfold_thms_tac _ [] = all_tac
- | unfold_thms_tac ctxt thms = Local_Defs.unfold0_tac ctxt (distinct Thm.eq_thm_prop thms);
+val unfold_thms_tac = Local_Defs.unfold0_tac;
fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
--- 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) =