Merge branch 'master' of github.com:jvanbruegge/binder_datatypes

Author: dtraytel

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)