Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 63853 d0e8921da311
parent 63313 0c956a9a0ac0
child 64430 1d85ac286c72 
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 12 16:08:27 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 12 16:51:55 2016 +0200
@@ -872,7 +872,8 @@
                 exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs;
 
               val nontriv_disc_defs = disc_defs
-                |> filter_out (member Thm.eq_thm_prop [unique_disc_no_def, alternate_disc_no_def]);
+                |> filter_out (member Thm.eq_thm_prop [unique_disc_no_def, alternate_disc_no_def,
+                  refl]);
 
               val disc_defs' =
                 map2 (fn k => fn def =>
isabelle