--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 08 12:01:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 08 14:48:19 2013 +0200
@@ -1114,9 +1114,9 @@
rtac conjI, rtac refl, rtac refl]) ks]) 1
end
-fun mk_dtor_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
+fun mk_dtor_map_unique_tac unfold_unique sym_map_comps {context = ctxt, prems = _} =
rtac unfold_unique 1 THEN
- unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
+ unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN
ALLGOALS (etac sym);
fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_mapss