# HG changeset patch
# User blanchet
# Date 1350565517 -7200
# Node ID cf441f4a358bbd66df109b49c43f4a824e44ef74
# Parent  4e17a6a0ef4fef4704688d3eda552784c0c5bbe0
renamed Isar-proof related options + changed semantics of Isar shrinking

diff -r 4e17a6a0ef4f -r cf441f4a358b NEWS
--- a/NEWS	Thu Oct 18 14:26:45 2012 +0200
+++ b/NEWS	Thu Oct 18 15:05:17 2012 +0200
@@ -185,6 +185,8 @@
   - Rationalized type encodings ("type_enc" option).
   - Renamed "kill_provers" subcommand to "kill"
   - Renamed options:
+      isar_proof ~> isar_proofs
+      isar_shrink_factor ~> isar_shrinkage
       max_relevant ~> max_facts
       relevance_thresholds ~> fact_thresholds
 
diff -r 4e17a6a0ef4f -r cf441f4a358b src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Thu Oct 18 14:26:45 2012 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Oct 18 15:05:17 2012 +0200
@@ -29,7 +29,7 @@
 
 (*** Now various verions with an increasing shrink factor ***)
 
-sledgehammer_params [isar_proof, isar_shrink_factor = 1]
+sledgehammer_params [isar_proofs, isar_shrinkage = 1]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -60,7 +60,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
 qed
 
-sledgehammer_params [isar_proof, isar_shrink_factor = 2]
+sledgehammer_params [isar_proofs, isar_shrinkage = 2]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -83,7 +83,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
 qed
 
-sledgehammer_params [isar_proof, isar_shrink_factor = 3]
+sledgehammer_params [isar_proofs, isar_shrinkage = 3]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -103,7 +103,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
 qed
 
-sledgehammer_params [isar_proof, isar_shrink_factor = 4]
+sledgehammer_params [isar_proofs, isar_shrinkage = 4]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -123,7 +123,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
 qed
 
-sledgehammer_params [isar_proof, isar_shrink_factor = 1]
+sledgehammer_params [isar_proofs, isar_shrinkage = 1]
 
 lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
 by (auto simp add: bigo_def bigo_pos_const)
diff -r 4e17a6a0ef4f -r cf441f4a358b src/HOL/Metis_Examples/Sets.thy
--- a/src/HOL/Metis_Examples/Sets.thy	Thu Oct 18 14:26:45 2012 +0200
+++ b/src/HOL/Metis_Examples/Sets.thy	Thu Oct 18 15:05:17 2012 +0200
@@ -21,7 +21,7 @@
 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
 by metis
 
-sledgehammer_params [isar_proof, isar_shrink_factor = 1]
+sledgehammer_params [isar_proofs, isar_shrinkage = 1]
 
 (*multiple versions of this example*)
 lemma (*equal_union: *)
@@ -70,7 +70,7 @@
   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
 qed
 
-sledgehammer_params [isar_proof, isar_shrink_factor = 2]
+sledgehammer_params [isar_proofs, isar_shrinkage = 2]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -107,7 +107,7 @@
   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
 qed
 
-sledgehammer_params [isar_proof, isar_shrink_factor = 3]
+sledgehammer_params [isar_proofs, isar_shrinkage = 3]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -124,7 +124,7 @@
   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
 qed
 
-sledgehammer_params [isar_proof, isar_shrink_factor = 4]
+sledgehammer_params [isar_proofs, isar_shrinkage = 4]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -140,7 +140,7 @@
   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
 qed
 
-sledgehammer_params [isar_proof, isar_shrink_factor = 1]
+sledgehammer_params [isar_proofs, isar_shrinkage = 1]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
diff -r 4e17a6a0ef4f -r cf441f4a358b src/HOL/Metis_Examples/Trans_Closure.thy
--- a/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Oct 18 14:26:45 2012 +0200
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Oct 18 15:05:17 2012 +0200
@@ -44,7 +44,7 @@
 
 lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-(* sledgehammer [isar_proof, isar_shrink_factor = 2] *)
+(* sledgehammer [isar_proofs, isar_shrinkage = 2] *)
 proof -
   assume A1: "f c = Intg x"
   assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
diff -r 4e17a6a0ef4f -r cf441f4a358b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Oct 18 14:26:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Oct 18 15:05:17 2012 +0200
@@ -94,8 +94,8 @@
    ("fact_thresholds", "0.45 0.85"),
    ("max_mono_iters", "smart"),
    ("max_new_mono_instances", "smart"),
-   ("isar_proof", "false"),
-   ("isar_shrink_factor", "1"),
+   ("isar_proofs", "false"),
+   ("isar_shrinkage", "10"),
    ("slice", "true"),
    ("minimize", "smart"),
    ("preplay_timeout", "3")]
@@ -112,14 +112,14 @@
    ("non_strict", "strict"),
    ("no_uncurried_aliases", "uncurried_aliases"),
    ("dont_learn", "learn"),
-   ("no_isar_proof", "isar_proof"),
+   ("no_isar_proofs", "isar_proofs"),
    ("dont_slice", "slice"),
    ("dont_minimize", "minimize")]
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
    "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
-   "isar_proof", "isar_shrink_factor", "timeout", "preplay_timeout"]
+   "isar_proofs", "isar_shrinkage", "timeout", "preplay_timeout"]
 
 val property_dependent_params = ["provers", "timeout"]
 
@@ -272,6 +272,13 @@
                     SOME n => n
                   | NONE => error ("Parameter " ^ quote name ^
                                    " must be assigned an integer value.")
+    fun lookup_real name =
+      case lookup name of
+        NONE => 0.0
+      | SOME s => case Real.fromString s of
+                    SOME n => n
+                  | NONE => error ("Parameter " ^ quote name ^
+                                   " must be assigned a real value.")
     fun lookup_real_pair name =
       case lookup name of
         NONE => (0.0, 0.0)
@@ -308,8 +315,8 @@
     val max_mono_iters = lookup_option lookup_int "max_mono_iters"
     val max_new_mono_instances =
       lookup_option lookup_int "max_new_mono_instances"
-    val isar_proof = lookup_bool "isar_proof"
-    val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
+    val isar_proofs = lookup_bool "isar_proofs"
+    val isar_shrinkage = Real.max (1.0, lookup_real "isar_shrinkage")
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize =
       if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
@@ -325,10 +332,9 @@
      lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
      learn = learn, fact_filter = fact_filter, max_facts = max_facts,
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
-     max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
-     isar_shrink_factor = isar_shrink_factor, slice = slice,
-     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
-     expect = expect}
+     max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
+     isar_shrinkage = isar_shrinkage, slice = slice, minimize = minimize,
+     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params
diff -r 4e17a6a0ef4f -r cf441f4a358b src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Oct 18 14:26:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Oct 18 15:05:17 2012 +0200
@@ -54,7 +54,7 @@
 
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
                  max_new_mono_instances, type_enc, strict, lam_trans,
-                 uncurried_aliases, isar_proof, isar_shrink_factor,
+                 uncurried_aliases, isar_proofs, isar_shrinkage,
                  preplay_timeout, ...} : params)
                silent (prover : prover) timeout i n state facts =
   let
@@ -72,9 +72,9 @@
        lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
        learn = false, fact_filter = NONE, max_facts = SOME (length facts),
        fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
-       max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
-       isar_shrink_factor = isar_shrink_factor, slice = false,
-       minimize = SOME false, timeout = timeout,
+       max_new_mono_instances = max_new_mono_instances,
+       isar_proofs = isar_proofs, isar_shrinkage = isar_shrinkage,
+       slice = false, minimize = SOME false, timeout = timeout,
        preplay_timeout = preplay_timeout, expect = ""}
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
@@ -236,8 +236,8 @@
 fun adjust_reconstructor_params override_params
         ({debug, verbose, overlord, blocking, provers, type_enc, strict,
          lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
-         fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proof,
-         isar_shrink_factor, slice, minimize, timeout, preplay_timeout, expect}
+         fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
+         isar_shrinkage, slice, minimize, timeout, preplay_timeout, expect}
          : params) =
   let
     fun lookup_override name default_value =
@@ -254,14 +254,13 @@
      lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
      learn = learn, fact_filter = fact_filter, max_facts = max_facts,
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
-     max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
-     isar_shrink_factor = isar_shrink_factor, slice = slice,
-     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
-     expect = expect}
+     max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
+     isar_shrinkage = isar_shrinkage, slice = slice, minimize = minimize,
+     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun maybe_minimize ctxt mode do_learn name
-        (params as {verbose, isar_proof, minimize, ...})
+        (params as {verbose, isar_proofs, minimize, ...})
         ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
         (result as {outcome, used_facts, run_time, preplay, message,
                     message_tail} : prover_result) =
@@ -282,7 +281,7 @@
                 <= Config.get ctxt auto_minimize_max_time
               fun prover_fast_enough () = can_min_fast_enough run_time
             in
-              if isar_proof then
+              if isar_proofs then
                 ((prover_fast_enough (), (name, params)), preplay)
               else
                 let val preplay = preplay () in
diff -r 4e17a6a0ef4f -r cf441f4a358b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Oct 18 14:26:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Oct 18 15:05:17 2012 +0200
@@ -33,8 +33,8 @@
      fact_thresholds : real * real,
      max_mono_iters : int option,
      max_new_mono_instances : int option,
-     isar_proof : bool,
-     isar_shrink_factor : int,
+     isar_proofs : bool,
+     isar_shrinkage : real,
      slice : bool,
      minimize : bool option,
      timeout : Time.time,
@@ -326,8 +326,8 @@
    fact_thresholds : real * real,
    max_mono_iters : int option,
    max_new_mono_instances : int option,
-   isar_proof : bool,
-   isar_shrink_factor : int,
+   isar_proofs : bool,
+   isar_shrinkage : real,
    slice : bool,
    minimize : bool option,
    timeout : Time.time,
@@ -642,7 +642,7 @@
           best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
         (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
                     uncurried_aliases, max_facts, max_mono_iters,
-                    max_new_mono_instances, isar_proof, isar_shrink_factor,
+                    max_new_mono_instances, isar_proofs, isar_shrinkage,
                     slice, timeout, preplay_timeout, ...})
         minimize_command
         ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
@@ -777,7 +777,7 @@
             fun sel_weights () = atp_problem_selection_weights atp_problem
             fun ord_info () = atp_problem_term_order_info atp_problem
             val ord = effective_term_order ctxt name
-            val full_proof = debug orelse isar_proof
+            val full_proof = debug orelse isar_proofs
             val args = arguments ctxt full_proof extra slice_timeout
                                  (ord, ord_info, sel_weights)
             val command =
@@ -883,7 +883,7 @@
            fn preplay =>
               let
                 val isar_params =
-                  (debug, isar_shrink_factor, pool, fact_names, sym_tab,
+                  (debug, verbose, isar_shrinkage, pool, fact_names, sym_tab,
                    atp_proof, goal)
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
@@ -891,7 +891,7 @@
                    subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
-                proof_text ctxt isar_proof isar_params num_chained
+                proof_text ctxt isar_proofs isar_params num_chained
                            one_line_params
               end,
            (if verbose then
diff -r 4e17a6a0ef4f -r cf441f4a358b src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Oct 18 14:26:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Oct 18 15:05:17 2012 +0200
@@ -23,7 +23,7 @@
   type one_line_params =
     play * string * (string * stature) list * minimize_command * int * int
   type isar_params =
-    bool * int * string Symtab.table * (string * stature) list vector
+    bool * bool * real * string Symtab.table * (string * stature) list vector
     * int Symtab.table * string proof * thm
 
   val smtN : string
@@ -52,6 +52,7 @@
 open ATP_Proof
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
+open Sledgehammer_Util
 
 structure String_Redirect = ATP_Proof_Redirect(
   type key = step_name
@@ -448,9 +449,9 @@
 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   | is_bad_free _ _ = false
 
-fun add_desired_line _ _ _ (line as Definition_Step (name, _, _)) (j, lines) =
+fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) =
     (j, line :: map (replace_dependencies_in_line (name, [])) lines)
-  | add_desired_line isar_shrink_factor fact_names frees
+  | add_desired_line fact_names frees
         (Inference_Step (name as (_, ss), t, rule, deps)) (j, lines) =
     (j + 1,
      if is_fact fact_names ss orelse
@@ -460,7 +461,7 @@
         (not (is_only_type_information t) andalso
          null (Term.add_tvars t []) andalso
          not (exists_subterm (is_bad_free frees) t) andalso
-         length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
+         length deps >= 2 andalso
          (* kill next to last line, which usually results in a trivial step *)
          j <> 1) then
        Inference_Step (name, t, rule, deps) :: lines  (* keep line *)
@@ -751,7 +752,7 @@
 
 val merge_timeout_slack = 1.2
 
-fun minimize_locally ctxt type_enc lam_trans proof =
+fun shrink_locally ctxt type_enc lam_trans isar_shrinkage proof =
   let
     (* Merging spots, greedy algorithm *)
     fun cost (Prove (_, _ , t, _)) = Term.size_of_term t
@@ -824,24 +825,26 @@
          SOME (front @ (the_list s0 @ s12 :: tail)))
         handle _ => NONE
       end
-    fun merge_steps proof [] = proof
-      | merge_steps proof (i :: is) = 
-        case try_merge proof i of 
-          NONE => merge_steps proof is
+    fun spill_shrinkage shrinkage = isar_shrinkage + shrinkage - 1.0
+    fun merge_steps _ proof [] = proof
+      | merge_steps shrinkage proof (i :: is) = 
+        if shrinkage < 1.5 then
+          merge_steps (spill_shrinkage shrinkage) proof is
+        else case try_merge proof i of
+          NONE => merge_steps (spill_shrinkage shrinkage) proof is
         | SOME proof' =>
-          merge_steps proof' (map (fn j => if j > i then j - 1 else j) is)
-  in merge_steps proof merge_spots end
+          merge_steps (shrinkage - 1.0) proof'
+            (map (fn j => if j > i then j - 1 else j) is)
+  in merge_steps isar_shrinkage proof merge_spots end
 
 type isar_params =
-  bool * int * string Symtab.table * (string * stature) list vector
+  bool * bool * real * string Symtab.table * (string * stature) list vector
   * int Symtab.table * string proof * thm
 
-fun isar_proof_text ctxt isar_proof_requested
-        (debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal)
-        (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
+fun isar_proof_text ctxt isar_proofs
+    (debug, verbose, isar_shrinkage, pool, fact_names, sym_tab, atp_proof, goal)
+    (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
-    val isar_shrink_factor =
-      (if isar_proof_requested then 1 else 2) * isar_shrink_factor
     val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
     val one_line_proof = one_line_proof_text 0 one_line_params
@@ -862,7 +865,7 @@
           |> repair_waldmeister_endgame
           |> rpair [] |-> fold_rev add_nontrivial_line
           |> rpair (0, [])
-          |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees)
+          |-> fold_rev (add_desired_line fact_names frees)
           |> snd
         val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
         val conjs =
@@ -908,42 +911,54 @@
           map (do_inf outer) infs
         val isar_proof =
           (if null params then [] else [Fix params]) @
-           (ref_graph
+          (ref_graph
            |> redirect_graph axioms tainted
            |> chain_direct_proof
            |> map (do_inf true)
            |> kill_duplicate_assumptions_in_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof
-           |> minimize_locally ctxt type_enc lam_trans)
-          |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
+           |> shrink_locally ctxt type_enc lam_trans
+                (if isar_proofs then isar_shrinkage else 1000.0))
+        val num_steps = length isar_proof
+        val isar_text =
+          string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
+                           isar_proof
       in
-        case isar_proof of
+        case isar_text of
           "" =>
-          if isar_proof_requested then
+          if isar_proofs then
             "\nNo structured proof available (proof too short)."
           else
             ""
         | _ =>
-          "\n\n" ^ (if isar_proof_requested then "Structured proof"
-                    else "Perhaps this will work") ^
-          ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_proof
+          "\n\n" ^
+          (if isar_proofs then
+             "Structured proof" ^
+             (if verbose then
+                " (" ^ string_of_int num_steps ^ " step" ^ plural_s num_steps ^
+                ")"
+              else
+                "")
+           else
+             "Perhaps this will work") ^
+          ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text
       end
     val isar_proof =
       if debug then
         isar_proof_of ()
       else case try isar_proof_of () of
         SOME s => s
-      | NONE => if isar_proof_requested then
+      | NONE => if isar_proofs then
                   "\nWarning: The Isar proof construction failed."
                 else
                   ""
   in one_line_proof ^ isar_proof end
 
-fun proof_text ctxt isar_proof isar_params num_chained
+fun proof_text ctxt isar_proofs isar_params num_chained
                (one_line_params as (preplay, _, _, _, _, _)) =
-  (if case preplay of Failed_to_Play _ => true | _ => isar_proof then
-     isar_proof_text ctxt isar_proof isar_params
+  (if case preplay of Failed_to_Play _ => true | _ => isar_proofs then
+     isar_proof_text ctxt isar_proofs isar_params
    else
      one_line_proof_text num_chained) one_line_params