--- a/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 22:39:46 2013 +0200
@@ -302,7 +302,7 @@
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
fun map_comp0_tac {context = ctxt, prems = _} =
- unfold_thms_tac ctxt (map_comp0_of_bnf bnf RS sym :: @{thms o_assoc id_o o_id}) THEN
+ unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
fun map_cong0_tac {context = ctxt, prems = _} =
mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
@@ -392,7 +392,7 @@
fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
fun map_comp0_tac {context = ctxt, prems = _} =
- unfold_thms_tac ctxt (map_comp0_of_bnf bnf RS sym :: @{thms o_assoc id_o o_id}) THEN
+ unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
fun map_cong0_tac {context = ctxt, prems = _} =
rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);