# HG changeset patch
# User blanchet
# Date 1391452322 -3600
# Node ID c3bb1cffce26cc718c16b736b7f01e6ee94fa686
# Parent  53569ca831f4ddd27fe7ed94cb1820ba768d5165
generate comments in Isar proofs

diff -r 53569ca831f4 -r c3bb1cffce26 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -174,7 +174,7 @@
                  else ([], rewrite_methods))
                 ||> massage_meths
             in
-              Prove ([], skos, l, t, [], ([], []), meths)
+              Prove ([], skos, l, t, [], ([], []), meths, "")
             end)
 
         val bot = atp_proof |> List.last |> #1
@@ -223,7 +223,7 @@
             accum
             |> (if tainted = [] then
                   cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
-                    (the_list predecessor, []), massage_meths metislike_methods))
+                    (the_list predecessor, []), massage_meths metislike_methods, ""))
                 else
                   I)
             |> rev
@@ -242,7 +242,7 @@
                  else metislike_methods)
                 |> massage_meths
 
-              fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths)
+              fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "")
               fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
             in
               if is_clause_tainted c then
@@ -256,7 +256,7 @@
                     steps_of_rest (prove [] deps)
                 | _ => steps_of_rest (prove [] deps))
               else
-                steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths)
+                steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths, "")
                   else prove [] deps)
             end
           | isar_steps outer predecessor accum (Cases cases :: infs) =
@@ -269,7 +269,7 @@
               val step =
                 Prove (maybe_show outer c [], [], l, t,
                   map isar_case (filter_out (null o snd) cases),
-                  (the_list predecessor, []), massage_meths metislike_methods)
+                  (the_list predecessor, []), massage_meths metislike_methods, "")
             in
               isar_steps outer (SOME l) (step :: accum) infs
             end
@@ -299,7 +299,6 @@
 
         fun str_of_preplay_outcome outcome =
           if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
-
         fun str_of_meth l meth =
           string_of_proof_method meth ^ " " ^
           str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
@@ -307,11 +306,17 @@
 
         fun trace_isar_proof label proof =
           if trace then
-            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^
-              "\n")
+            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
+              string_of_isar_proof (comment_isar_proof comment_of proof) ^ "\n")
           else
             ()
 
+        fun comment_of l (meth :: _) =
+          (case (verbose,
+              Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of
+            (false, Played _) => ""
+          | (_, outcome) => string_of_play_outcome outcome)
+
         val (play_outcome, isar_proof) =
           canonical_isar_proof
           |> tap (trace_isar_proof "Original")
@@ -322,11 +327,12 @@
                 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
           |> tap (trace_isar_proof "Minimized")
           |> `(preplay_outcome_of_isar_proof (!preplay_data))
+          ||> comment_isar_proof comment_of
           ||> chain_isar_proof
           ||> kill_useless_labels_in_isar_proof
           ||> relabel_isar_proof_nicely
       in
-        (case string_of_isar_proof (K (K "")) isar_proof of
+        (case string_of_isar_proof isar_proof of
           "" =>
           if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
           else ""
diff -r 53569ca831f4 -r c3bb1cffce26 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -32,7 +32,7 @@
       | collect_steps [] accum = accum
       | collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum)
     and collect_step (Let _) x = x
-      | collect_step (step as Prove (_, _, l, _, subproofs, _, _)) x =
+      | collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x =
         (case collect_subproofs subproofs x of
           ([], accu) => ([], accu)
         | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
@@ -55,16 +55,16 @@
       | update_steps (step :: steps) updates = update_step step (update_steps steps updates)
     and update_step step (steps, []) = (step :: steps, [])
       | update_step (step as Let _) (steps, updates) = (step :: steps, updates)
-      | update_step (Prove (qs, xs, l, t, subproofs, facts, meths))
-          (steps, updates as Prove (qs', xs', l', t', subproofs', facts', meths') :: updates') =
-        let
-          val (subproofs, updates) =
-            if l = l' then update_subproofs subproofs' updates'
-            else update_subproofs subproofs updates
-        in
-          if l = l' then (Prove (qs', xs', l', t', subproofs, facts', meths') :: steps, updates)
-          else (Prove (qs, xs, l, t, subproofs, facts, meths) :: steps, updates)
-        end
+      | update_step (Prove (qs, xs, l, t, subproofs, facts, meths, comment))
+          (steps,
+           updates as Prove (qs', xs', l', t', subproofs', facts', meths', comment') :: updates') =
+        (if l = l' then
+           update_subproofs subproofs' updates'
+           |>> (fn subproofs' => Prove (qs', xs', l', t', subproofs', facts', meths', comment'))
+         else
+           update_subproofs subproofs updates
+           |>> (fn subproofs => Prove (qs, xs, l, t, subproofs, facts, meths, comment)))
+        |>> (fn step => step :: steps)
     and update_subproofs [] updates = ([], updates)
       | update_subproofs steps [] = (steps, [])
       | update_subproofs (proof :: subproofs) updates =
@@ -91,8 +91,8 @@
     inter (op =) (filter (is_method_hopeful l1) meths1) (filter (is_method_hopeful l2) meths2)
   end
 
-fun try_merge preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1))
-      (Prove (qs2, fix, l2, t, subproofs2, (lfs2, gfs2), meths2)) =
+fun try_merge preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
+      (Prove (qs2, fix, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) =
     (case merge_methods preplay_data (l1, meths1) (l2, meths2) of
       [] => NONE
     | meths =>
@@ -100,7 +100,8 @@
         val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
         val gfs = union (op =) gfs1 gfs2
       in
-        SOME (Prove (qs2, fix, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths))
+        SOME (Prove (qs2, fix, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths,
+          comment1 ^ comment2))
       end)
   | try_merge _ _ _ = NONE
 
@@ -128,9 +129,9 @@
 
       val (get_successors, replace_successor) =
         let
-          fun add_refs (Let _) = I
-            | add_refs (Prove (_, _, v, _, _, (lfs, _), _)) =
-              fold (fn key => Canonical_Label_Tab.cons_list (key, v)) lfs
+          fun add_refs (Prove (_, _, l, _, _, (lfs, _), _, _)) =
+              fold (fn key => Canonical_Label_Tab.cons_list (key, l)) lfs
+            | add_refs _ = I
 
           val tab =
             Canonical_Label_Tab.empty
@@ -151,11 +152,11 @@
         end
 
       (* elimination of trivial, one-step subproofs *)
-      fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs =
+      fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) comment subs nontriv_subs =
         if null subs orelse not (compress_further ()) then
           let
             val subproofs = List.revAppend (nontriv_subs, subs)
-            val step = Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths)
+            val step = Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)
           in
             set_preplay_outcomes_of_isar_step ctxt time preplay_data step [(meth, Played time)];
             step
@@ -165,7 +166,7 @@
             (sub as Proof (_, assms, sub_steps)) :: subs =>
             (let
               (* trivial subproofs have exactly one "Prove" step *)
-              val [Prove (_, [], l', _, [], (lfs', gfs'), meths')] = sub_steps
+              val [Prove (_, [], l', _, [], (lfs', gfs'), meths', _)] = sub_steps
 
               (* only touch proofs that can be preplayed sucessfully *)
               val Played time' = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l'
@@ -175,7 +176,7 @@
               val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
               val gfs'' = union (op =) gfs' gfs
               val meths'' as _ :: _ = merge_methods (!preplay_data) (l', meths') (l, meths)
-              val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'')
+              val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'', comment)
 
               (* check if the modified step can be preplayed fast enough *)
               val timeout = slackify_merge_timeout (Time.+ (time, time'))
@@ -183,20 +184,20 @@
             in
               decrement_step_count (); (* l' successfully eliminated! *)
               map (replace_successor l' [l]) lfs';
-              elim_one_subproof time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs
+              elim_one_subproof time'' qs fix l t lfs'' gfs'' meths comment subs nontriv_subs
             end
             handle Bind =>
-              elim_one_subproof time qs fix l t lfs gfs meths subs (sub :: nontriv_subs))
+              elim_one_subproof time qs fix l t lfs gfs meths comment subs (sub :: nontriv_subs))
           | _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof")
 
-      fun elim_subproofs (step as Let _) = step
-        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths)) =
+      fun elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)) =
           if subproofs = [] then
             step
           else
             (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of
-              Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs []
+              Played time => elim_one_subproof time qs fix l t lfs gfs meths comment subproofs []
             | _ => step)
+        | elim_subproofs step = step
 
       fun compress_top_level steps =
         let
@@ -218,8 +219,8 @@
 
           val candidates =
             let
-              fun add_cand (_, Let _) = I
-                | add_cand (i, Prove (_, _, l, t, _, _, _)) = cons (i, l, size_of_term t)
+              fun add_cand (i, Prove (_, _, l, t, _, _, _, _)) = cons (i, l, size_of_term t)
+                | add_cand _ = I
             in
               (steps
                |> split_last |> fst (* keep last step *)
@@ -228,7 +229,7 @@
 
           fun try_eliminate (i, l, _) labels steps =
             let
-              val ((cand as Prove (_, _, _, _, _, (lfs, _), _)) :: steps') = drop i steps
+              val ((cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps') = drop i steps
 
               val succs = collect_successors steps' labels
 
@@ -292,9 +293,9 @@
         steps |> map (fn step => step |> compress_further () ? compress_sub_levels)
               |> compress_further () ? compress_top_level
       and compress_sub_levels (step as Let _) = step
-        | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths)) =
+        | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
           (* compress subproofs *)
-          Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths)
+          Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment)
           (* eliminate trivial subproofs *)
           |> compress_further () ? elim_subproofs
     in
diff -r 53569ca831f4 -r c3bb1cffce26 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -25,19 +25,21 @@
 open Sledgehammer_Isar_Proof
 open Sledgehammer_Isar_Preplay
 
-fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, meths)) =
+fun keep_fastest_method_of_isar_step preplay_data
+      (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
     Prove (qs, xs, l, t, subproofs, facts,
-      meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @)
+      meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @,
+      comment)
   | keep_fastest_method_of_isar_step _ step = step
 
 val slack = seconds 0.1
 
 fun minimize_isar_step_dependencies ctxt preplay_data
-      (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _)) =
+      (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
     (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
       Played time =>
       let
-        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)
+        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
 
         fun minimize_facts _ time min_facts [] = (time, min_facts)
           | minimize_facts mk_step time min_facts (f :: facts) =
@@ -76,7 +78,7 @@
         else
           (used, accu))
     and process_used_step step = step |> postproc_step |> process_used_step_subproofs
-    and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)) =
+    and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) =
       let
         val (used, subproofs) =
           map process_proof subproofs
@@ -84,7 +86,7 @@
           |>> Ord_List.unions label_ord
           |>> fold (Ord_List.insert label_ord) lfs
       in
-        (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths))
+        (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment))
       end
   in
     snd o process_proof
diff -r 53569ca831f4 -r c3bb1cffce26 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -52,9 +52,9 @@
 
     fun enrich_with_proof (Proof (_, assms, isar_steps)) =
       enrich_with_assms assms #> fold enrich_with_step isar_steps
-    and enrich_with_step (Let _) = I
-      | enrich_with_step (Prove (_, _, l, t, subproofs, _, _)) =
+    and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) =
         enrich_with_fact l t #> fold enrich_with_proof subproofs
+      | enrich_with_step _ = I
   in
     enrich_with_proof proof ctxt
   end
@@ -88,7 +88,7 @@
 
     val concl = 
       (case try List.last steps of
-        SOME (Prove (_, [], _, t, _, _, _)) => t
+        SOME (Prove (_, [], _, t, _, _, _, _)) => t
       | _ => raise Fail "preplay error: malformed subproof")
 
     val var_idx = maxidx_of_term concl + 1
@@ -100,8 +100,8 @@
     |> Skip_Proof.make_thm thy
   end
 
-(* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
+(* may throw exceptions *)
+fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) =
   let
     val goal =
       (case xs of
@@ -122,18 +122,18 @@
           Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
         end)
 
-    val facts =
-      resolve_fact_names ctxt fact_names
+    val assmsp =
+      resolve_fact_names ctxt facts
       |>> append (map (thm_of_proof ctxt) subproofs)
 
     fun prove () =
       Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
-        HEADGOAL (tac_of_proof_method ctxt facts meth))
+        HEADGOAL (tac_of_proof_method ctxt assmsp meth))
       handle ERROR msg => error ("Preplay error: " ^ msg)
 
     val play_outcome = take_time timeout prove ()
   in
-    (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
+    (if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
      play_outcome)
   end
 
@@ -164,7 +164,7 @@
     Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
 
 fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
-      (step as Prove (_, _, l, _, _, _, meths)) meths_outcomes0 =
+      (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
     let
       fun lazy_preplay meth =
         Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
@@ -207,7 +207,7 @@
   #> get_best_method_outcome Lazy.force
   #> fst
 
-fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths)) =
+fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) =
     Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths))
   | forced_outcome_of_step _ _ = Played Time.zeroTime
 
diff -r 53569ca831f4 -r c3bb1cffce26 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -20,7 +20,7 @@
   and isar_step =
     Let of term * term |
     Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
-      * facts * proof_method list
+      * facts * proof_method list * string
 
   val no_label : label
 
@@ -41,13 +41,13 @@
 
   val canonical_label_ord : (label * label) -> order
 
+  val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof
   val chain_isar_proof : isar_proof -> isar_proof
   val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
   val relabel_isar_proof_canonically : isar_proof -> isar_proof
   val relabel_isar_proof_nicely : isar_proof -> isar_proof
 
-  val string_of_isar_proof : Proof.context -> int -> int ->
-    (label -> proof_method list -> string) -> isar_proof -> string
+  val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string
 end;
 
 structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
@@ -71,7 +71,7 @@
 and isar_step =
   Let of term * term |
   Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
-    * facts * proof_method list
+    * facts * proof_method list * string
 
 val no_label = ("", ~1)
 
@@ -81,16 +81,16 @@
 
 fun steps_of_isar_proof (Proof (_, _, steps)) = steps
 
-fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l
+fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
   | label_of_isar_step _ = NONE
 
-fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _)) = subs
+fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs
   | subproofs_of_isar_step _ = []
 
-fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _)) = facts
+fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts
   | facts_of_isar_step _ = ([], [])
 
-fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths)) = meths
+fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths
   | proof_methods_of_isar_step _ = []
 
 fun fold_isar_step f step =
@@ -101,8 +101,8 @@
   let
     fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps)
     and map_step (step as Let _) = f step
-      | map_step (Prove (qs, xs, l, t, subs, facts, meths)) =
-        f (Prove (qs, xs, l, t, map map_proof subs, facts, meths))
+      | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
+        f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment))
   in map_proof end
 
 val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
@@ -114,12 +114,17 @@
   type key = label
   val ord = canonical_label_ord)
 
+fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) =
+    Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths)
+  | comment_isar_step _ step = step
+fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of)
+
 fun chain_qs_lfs NONE lfs = ([], lfs)
   | chain_qs_lfs (SOME l0) lfs =
     if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
-fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths)) =
+fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
     let val (qs', lfs) = chain_qs_lfs lbl lfs in
-      Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths)
+      Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
     end
   | chain_isar_step _ step = step
 and chain_isar_steps _ [] = []
@@ -136,8 +141,8 @@
 
     fun kill_label l = if member (op =) used_ls l then l else no_label
 
-    fun kill_step (Prove (qs, xs, l, t, subs, facts, meths)) =
-        Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths)
+    fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
+        Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment)
       | kill_step step = step
     and kill_proof (Proof (fix, assms, steps)) =
       Proof (fix, map (apfst kill_label) assms, map kill_step steps)
@@ -150,14 +155,15 @@
     fun next_label l (next, subst) =
       let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
 
-    fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths)) (accum as (_, subst)) =
+    fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment))
+          (accum as (_, subst)) =
         let
           val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
           val ((subs', l'), accum') = accum
             |> fold_map relabel_proof subs
             ||>> next_label l
         in
-          (Prove (qs, fix, l', t, subs', (lfs', gfs), meths), accum')
+          (Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum')
         end
       | relabel_step step accum = (step, accum)
     and relabel_proof (Proof (fix, assms, steps)) =
@@ -181,13 +187,14 @@
           (l', (next + 1, (l, l') :: subst))
         end
 
-    fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths)) (accum as (_, subst)) =
+    fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment))
+          (accum as (_, subst)) =
         let
           val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
           val (l', accum' as (next', subst')) = next_label depth have_prefix l accum
           val subs' = map (relabel_proof subst' (depth + 1)) subs
         in
-          (Prove (qs, xs, l', t, subs', (lfs', gfs), meths), accum')
+          (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum')
         end
       | relabel_step _ step accum = (step, accum)
     and relabel_proof subst depth (Proof (fix, assms, steps)) =
@@ -201,7 +208,7 @@
 
 val indent_size = 2
 
-fun string_of_isar_proof ctxt i n comment_of proof =
+fun string_of_isar_proof ctxt i n proof =
   let
     (* Make sure only type constraints inserted by the type annotation code are printed. *)
     val ctxt =
@@ -298,7 +305,7 @@
     and add_step ind (Let (t1, t2)) =
         add_str (of_indent ind ^ "let ")
         #> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n"
-      | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meths as meth :: _)) =
+      | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meths as meth :: _, comment)) =
         add_step_pre ind qs subs
         #> (case xs of
              [] => add_str (of_have qs (length subs) ^ " ")
@@ -307,9 +314,7 @@
         #> add_term t
         #> add_str (" " ^
              of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
-             (case comment_of l meths of
-               "" => ""
-             | comment => " (* " ^ comment ^ " *)") ^ "\n")
+             (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
     and add_steps ind = fold (add_step ind)
     and of_proof ind ctxt (Proof (xs, assms, steps)) =
       ("", ctxt)
@@ -321,7 +326,7 @@
     (* One-step Metis proofs are pointless; better use the one-liner directly. *)
     (case proof of
       Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
-    | Proof ([], [], [Prove (_, [], _, _, [], _, Metis_Method _ :: _)]) => ""
+    | Proof ([], [], [Prove (_, [], _, _, [], _, Metis_Method _ :: _, _)]) => ""
     | _ =>
       (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
       of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^