# HG changeset patch
# User nipkow
# Date 1480435090 -3600
# Node ID ff59fe6b6f6ae6041946fae9228633e8ed1c7e1d
# Parent  fc2835a932d9e3118067b82493df112614a5a515# Parent  172f3a047f4aecfccef53e2ceaffad9054eaa423
merged

diff -r 172f3a047f4a -r ff59fe6b6f6a NEWS
--- a/NEWS	Tue Nov 29 10:53:52 2016 +0100
+++ b/NEWS	Tue Nov 29 16:58:10 2016 +0100
@@ -6,6 +6,11 @@
 New in this Isabelle version
 ----------------------------
 
+* (Co)datatype package:
+  - The 'size_gen_o_map' lemma is no longer generated for datatypes
+    with type class annotations. As a result, the tactic that derives
+    it no longer fails on nested datatypes. Slight INCOMPATIBILITY.
+
 
 
 New in Isabelle2016-1 (December 2016)
diff -r 172f3a047f4a -r ff59fe6b6f6a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Nov 29 10:53:52 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Nov 29 16:58:10 2016 +0100
@@ -2825,6 +2825,9 @@
   thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
 qed
 
+lemmas mult_cancel_add_mset =
+  mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral]
+
 lemma mult_cancel_max:
   assumes "trans s" and "irrefl s"
   shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
diff -r 172f3a047f4a -r ff59fe6b6f6a src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Nov 29 10:53:52 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Nov 29 16:58:10 2016 +0100
@@ -341,7 +341,8 @@
               fold_rev (curry (op @) o #co_rec_o_maps o the o #fp_co_induct_sugar) fp_sugars [];
 
             val size_gen_o_map_thmss =
-              if nested_size_gen_o_maps_complete then
+              if nested_size_gen_o_maps_complete
+                 andalso forall (fn TFree (_, S) => S = @{sort type}) As then
                 @{map 3} (fn goal => fn size_def => fn rec_o_map =>
                     Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
                       mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)