src/HOL/Tools/BNF/bnf_def_tactics.ML
changeset 67223 711eec20aecd
parent 67222 19809bc9d7ff
child 67399 eab6ce8368fa
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sun Dec 17 08:42:59 2017 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Dec 18 11:56:12 2017 +0100
@@ -263,7 +263,7 @@
      REPEAT_DETERM (HEADGOAL (resolve_tac ctxt (maps (fn thm =>
        [thm RS trans, thm RS @{thm trans[rotated, OF sym]}]) rel_map))) THEN
      HEADGOAL (rtac ctxt iffI) THEN
-     last_tac iffD1 THEN  print_tac ctxt "baz" THEN last_tac iffD2)
+     last_tac iffD1 THEN last_tac iffD2)
   end;
 
 fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =