# HG changeset patch
# User blanchet
# Date 1425397065 -3600
# Node ID 5f56d4ff6635f3f1c7fb25ef06340712103b1c47
# Parent  012c6165bbd2f19c16d9f6772a0e38b85ce634b9
strengthened 'size' tactic for examples like datatype (dead 'a, 'b) y = Y "'a * 'b"

diff -r 012c6165bbd2 -r 5f56d4ff6635 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 03 16:37:45 2015 +0100
@@ -65,7 +65,7 @@
   unfold_thms_tac ctxt [size_def] THEN
   HEADGOAL (rtac (rec_o_map RS trans) THEN'
     asm_simp_tac (ss_only (inj_maps @ size_maps @ size_gen_o_map_simps) ctxt)) THEN
-  IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
+  IF_UNSOLVED (unfold_thms_tac ctxt @{thms id_def o_def} THEN HEADGOAL (rtac refl));
 
 fun mk_size_neq ctxt cts exhaust sizes =
   HEADGOAL (rtac (Ctr_Sugar_Util.cterm_instantiate_pos (map SOME cts) exhaust)) THEN