--- a/src/HOL/ex/Sketch_and_Explore.thy Mon Mar 11 21:11:23 2024 +0100
+++ b/src/HOL/ex/Sketch_and_Explore.thy Mon Mar 11 21:46:31 2024 +0100
@@ -26,7 +26,6 @@
t
|> singleton (Syntax.uncheck_terms ctxt)
|> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt
- \<comment> \<open>TODO pointless to annotate explicit fixes in term\<close>
|> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
|> Sledgehammer_Util.simplify_spaces
|> ATP_Util.maybe_quote ctxt;
@@ -41,7 +40,6 @@
let
val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt;
val prefix = replicate_string indent " ";
- \<comment> \<open>TODO consider pre-existing indentation -- how?\<close>
val prefix_sep = "\n" ^ prefix ^ " and ";
val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl;
val if_s = if null assms then NONE