# HG changeset patch
# User blanchet
# Date 1406280370 -7200
# Node ID 09d2b853b20c3b86de6b1fad3a3d025d5ef70bd4
# Parent  232954f7df1c5eb1b3d3c8fb67da00693da52f68
tuning

diff -r 232954f7df1c -r 09d2b853b20c src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Jul 24 23:01:23 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Jul 25 11:26:10 2014 +0200
@@ -1,7 +1,8 @@
 (*  Title:      HOL/Tools/BNF/bnf_def.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012
+    Author:     Martin Desharnais, TU Muenchen
+    Copyright   2012, 2013, 2014
 
 Definition of bounded natural functors.
 *)
diff -r 232954f7df1c -r 09d2b853b20c src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Jul 24 23:01:23 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Jul 25 11:26:10 2014 +0200
@@ -1,7 +1,8 @@
 (*  Title:      HOL/Tools/BNF/bnf_def_tactics.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012
+    Author:     Martin Desharnais, TU Muenchen
+    Copyright   2012, 2013, 2014
 
 Tactics for definition of bounded natural functors.
 *)
diff -r 232954f7df1c -r 09d2b853b20c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 24 23:01:23 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Jul 25 11:26:10 2014 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Tools/BNF/bnf_fp_def_sugar.ML
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012, 2013
+    Author:     Martin Desharnais, TU Muenchen
+    Copyright   2012, 2013, 2014
 
 Sugared datatype and codatatype constructions.
 *)
diff -r 232954f7df1c -r 09d2b853b20c src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Jul 24 23:01:23 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Jul 25 11:26:10 2014 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012
+    Author:     Martin Desharnais, TU Muenchen
+    Copyright   2012, 2013, 2014
 
 Tactics for datatype and codatatype sugar.
 *)
@@ -234,13 +235,12 @@
   rtac dtor_rel_coinduct 1 THEN
   EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
     fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
-      (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
-        (dtac (rotate_prems (~1) ((cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct] @{thm
-        arg_cong2}) RS iffD1)) THEN'
+      rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
+        (dtac (rotate_prems (~1)
+          (cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct] @{thm arg_cong2} RS iffD1)) THEN'
         atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN'
-        REPEAT_DETERM o etac conjE))) 1 THEN
-      unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels
-        @ simp_thms') THEN
+        REPEAT_DETERM o etac conjE)) 1 THEN
+      unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN
       unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
         abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def
         rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl]
diff -r 232954f7df1c -r 09d2b853b20c src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jul 24 23:01:23 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Jul 25 11:26:10 2014 +0200
@@ -1,7 +1,8 @@
 (*  Title:      HOL/Tools/BNF/bnf_fp_util.ML
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012, 2013
+    Author:     Martin Desharnais, TU Muenchen
+    Copyright   2012, 2013, 2014
 
 Shared library for the datatype and codatatype constructions.
 *)