# HG changeset patch
# User blanchet
# Date 1408433697 -7200
# Node ID c52255a711149786fadb70c88febdd89a08e3153
# Parent  2371bff894f97dd075de003600347551b8f7e339
robustified tactics

diff -r 2371bff894f9 -r c52255a71114 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Tue Aug 19 09:34:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Tue Aug 19 09:34:57 2014 +0200
@@ -16,7 +16,7 @@
 open BNF_FP_N2M_Sugar
 open BNF_LFP_Rec_Sugar
 
-val nested_simps = @{thms id_def split comp_def fst_conv snd_conv};
+val nested_simps = @{thms o_def[abs_def] id_def split fst_conv snd_conv};
 
 fun is_new_datatype ctxt s =
   (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
diff -r 2371bff894f9 -r c52255a71114 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Aug 19 09:34:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Aug 19 09:34:57 2014 +0200
@@ -64,7 +64,8 @@
   funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong);
 
 val rec_o_map_simp_thms =
-  @{thms o_def id_def case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def};
+  @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod
+      BNF_Comp.id_bnf_comp_def};
 
 fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
     ctor_rec_o_map =
@@ -72,8 +73,8 @@
   HEADGOAL (rtac (ctor_rec_o_map RS trans) THEN'
     CONVERSION Thm.eta_long_conversion THEN'
     asm_simp_tac (ss_only (pre_map_defs @
-      distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @
-      rec_o_map_simp_thms) ctxt));
+        distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simp_thms)
+      ctxt));
 
 val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};