# HG changeset patch
# User desharna
# Date 1411718315 -7200
# Node ID 126c353540fc081be30ce08a10c14f9d8da332f6
# Parent  271829a473ed1ac5db4bf3420a3469880966bcc6
make 'case_transfer' tactic more robust

diff -r 271829a473ed -r 126c353540fc src/HOL/Datatype_Examples/Misc_Codatatype.thy
--- a/src/HOL/Datatype_Examples/Misc_Codatatype.thy	Thu Sep 25 18:47:32 2014 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Codatatype.thy	Fri Sep 26 09:58:35 2014 +0200
@@ -36,6 +36,8 @@
 codatatype 'a multi_live_direct8 = MultiLiveDirect8 'a 'a 'a 'a 'a 'a 'a 'a
 codatatype 'a multi_live_direct9 = MultiLiveDirect9 'a 'a 'a 'a 'a 'a 'a 'a 'a
 
+datatype 'a live_and_fun = LiveAndFun nat "nat \<Rightarrow> 'a"
+
 codatatype lambda =
   Var string |
   App lambda lambda |
diff -r 271829a473ed -r 126c353540fc src/HOL/Datatype_Examples/Misc_Datatype.thy
--- a/src/HOL/Datatype_Examples/Misc_Datatype.thy	Thu Sep 25 18:47:32 2014 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy	Fri Sep 26 09:58:35 2014 +0200
@@ -34,6 +34,8 @@
 datatype (discs_sels) 'a multi_live_direct8 = MultiLiveDirect8 'a 'a 'a 'a 'a 'a 'a 'a
 datatype (discs_sels) 'a multi_live_direct9 = MultiLiveDirect9 'a 'a 'a 'a 'a 'a 'a 'a 'a
 
+datatype 'a live_and_fun = LiveAndFun nat "nat \<Rightarrow> 'a"
+
 datatype (discs_sels) hfset = HFset "hfset fset"
 
 datatype (discs_sels) lambda =
diff -r 271829a473ed -r 126c353540fc src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Sep 25 18:47:32 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Sep 26 09:58:35 2014 +0200
@@ -110,8 +110,9 @@
     HEADGOAL (etac rel_cases) THEN
     ALLGOALS (hyp_subst_tac ctxt) THEN
     unfold_thms_tac ctxt cases THEN
-    ALLGOALS (fn k => (select_prem_tac n (dtac asm_rl) k THEN' rotate_tac ~1) k) THEN
-    ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac rel_funD))
+    ALLGOALS (fn k => (select_prem_tac n (dtac asm_rl) k) k) THEN
+    ALLGOALS (REPEAT_DETERM o (rotate_tac ~1 THEN' dtac @{thm rel_funD} THEN'
+      (atac THEN' etac thin_rl ORELSE' rtac refl)) THEN' atac)
   end;
 
 fun mk_ctr_transfer_tac ctxt rel_intros rel_eqs =