Remove debug print statements from tactic

jvanbruegge · Sep 26, 2024 · ef74954 · ef74954
1 parent 087af5b
commit ef74954
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/Tools/mrbnf_sugar.ML b/Tools/mrbnf_sugar.ML
@@ -295,12 +295,10 @@ fun create_binder_datatype (spec : spec) lthy =
             REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms UNIV_I UN_I singletonI TrueI}),
             IF_UNSOLVED o EVERY' [
               etac ctxt @{thm contrapos_pp},
-              K (print_tac ctxt "bar"),
               K (Local_Defs.unfold0_tac ctxt @{thms Un_iff de_Morgan_disj}),
               REPEAT_DETERM o etac ctxt conjE,
               assume_tac ctxt,
-              TRY o rtac ctxt @{thm UNIV_I},
-              K (print_tac ctxt "foo")
+              TRY o rtac ctxt @{thm UNIV_I}
             ],
             IF_UNSOLVED o K no_tac
           ])) prems)