# HG changeset patch
# User wenzelm
# Date 1464879940 -7200
# Node ID bcf4828bb125a0d0e648f592808ef3723b1c9026
# Parent  fe92356ade422d2e752fa1cd052d1dcd934de25d
clarified aliases (no warning for duplicates);

diff -r fe92356ade42 -r bcf4828bb125 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
--- 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});
 
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) =