more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal);

--- a/src/HOL/Eisbach/Tests.thy	Tue Sep 17 17:06:05 2019 +0200
+++ b/src/HOL/Eisbach/Tests.thy	Wed Sep 18 20:10:15 2019 +0200
@@ -166,7 +166,7 @@
     done
 
   (* Cut tests *)
-  fix A B C
+  fix A B C D
 
   have "D \<and> C  \<Longrightarrow> A \<and> B  \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
     by (((match premises in I: "P \<and> Q" (cut)

--- a/src/Pure/Isar/obtain.ML	Tue Sep 17 17:06:05 2019 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Sep 18 20:10:15 2019 +0200
@@ -201,7 +201,7 @@
 
     val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
 
-    val ((vars, propss, binds, binds'), params_ctxt) =
+    val ((vars, propss, binds, binds', _), params_ctxt) =
       prep_stmt (raw_decls @ raw_fixes) (raw_prems @ map #2 raw_concls) thesis_ctxt;
     val (decls, fixes) = chop (length raw_decls) vars ||> map #2;
     val (premss, conclss) = chop (length raw_prems) propss;

--- a/src/Pure/Isar/proof.ML	Tue Sep 17 17:06:05 2019 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Sep 18 20:10:15 2019 +0200
@@ -645,7 +645,7 @@
     val ctxt = context_of state;
 
     val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls;
-    val ((params, prems_propss, concl_propss, result_binds), _) =
+    val ((params, prems_propss, concl_propss, result_binds, _), _) =
       prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt;
     val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss;
   in
@@ -812,7 +812,7 @@
     val ctxt = context_of state;
 
     (*vars*)
-    val ((vars, propss, _, binds'), vars_ctxt) =
+    val ((vars, propss, _, binds', text'), vars_ctxt) =
       prep_stmt (raw_decls @ raw_fixes) (map snd raw_defs) ctxt;
     val (decls, fixes) = chop (length raw_decls) vars;
     val show_term = Syntax.string_of_term vars_ctxt;
@@ -1057,7 +1057,7 @@
         (if strict_asm then Assumption.assume_export else Assumption.presume_export);
 
     (*params*)
-    val ((params, assumes_propss, shows_propss, result_binds), params_ctxt) = ctxt
+    val ((params, assumes_propss, shows_propss, result_binds, result_text), params_ctxt) = ctxt
       |> prep_statement raw_fixes (map snd raw_assumes) (map snd raw_shows);
 
     (*prems*)
@@ -1089,6 +1089,7 @@
         val export = map export0 #> Variable.export result_ctxt ctxt';
       in
         state'
+        |> map_context (Variable.declare_term result_text)
         |> local_results (results_bindings ~~ burrow export results)
         |-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
         |> after_qed (result_ctxt, results)

--- a/src/Pure/Isar/proof_context.ML	Tue Sep 17 17:06:05 2019 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Sep 18 20:10:15 2019 +0200
@@ -172,18 +172,18 @@
   val cert_stmt:
     (binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context ->
     (((binding * typ option * mixfix) * (string * term)) list * term list list *
-      (indexname * term) list * (indexname * term) list) * Proof.context
+      (indexname * term) list * (indexname * term) list * term) * Proof.context
   val read_stmt:
     (binding * string option * mixfix) list -> (string * string list) list list -> Proof.context ->
     (((binding * typ option * mixfix) * (string * term)) list * term list list *
-      (indexname * term) list * (indexname * term) list) * Proof.context
+      (indexname * term) list * (indexname * term) list * term) * Proof.context
   val cert_statement: (binding * typ option * mixfix) list ->
     (term * term list) list list -> (term * term list) list list -> Proof.context ->
-    ((string * term) list * term list list * term list list * (indexname * term option) list) *
+    ((string * term) list * term list list * term list list * (indexname * term option) list * term) *
       Proof.context
   val read_statement: (binding * string option * mixfix) list ->
     (string * string list) list list -> (string * string list) list list -> Proof.context ->
-    ((string * term) list * term list list * term list list * (indexname * term option) list) *
+    ((string * term) list * term list list * term list list * (indexname * term option) list * term) *
       Proof.context
   val print_syntax: Proof.context -> unit
   val print_abbrevs: bool -> Proof.context -> unit
@@ -1363,23 +1363,27 @@
       |> export_binds params_ctxt ctxt params
       |> map (apsnd the);
 
+    val text' =
+      Logic.close_prop params [] (Logic.mk_conjunction_list (flat propss))
+      |> singleton (Variable.export_terms params_ctxt ctxt);
+
     val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt;
-  in ((vars' ~~ params, propss, binds, binds'), params_ctxt) end;
+  in ((vars' ~~ params, propss, binds, binds', text'), params_ctxt) end;
 
 fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
   let
-    val ((fixes, (assumes, shows), binds), ctxt') = ctxt
+    val ((fixes, (assumes, shows), binds, text'), ctxt') = ctxt
       |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows)
-      |-> (fn (vars, propss, binds, _) =>
+      |-> (fn (vars, propss, binds, _, text') =>
         fold Variable.bind_term binds #>
-        pair (map #2 vars, chop (length raw_assumes) propss, binds));
+        pair (map #2 vars, chop (length raw_assumes) propss, binds, text'));
     val binds' =
       (Auto_Bind.facts ctxt' (flat shows) @
         (case try List.last (flat shows) of
           NONE => []
         | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds))
       |> export_binds ctxt' ctxt fixes;
-  in ((fixes, assumes, shows, binds'), ctxt') end;
+  in ((fixes, assumes, shows, binds', text'), ctxt') end;
 
 in
 

--- a/src/Pure/Isar/specification.ML	Tue Sep 17 17:06:05 2019 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Sep 18 20:10:15 2019 +0200
@@ -204,7 +204,7 @@
 fun gen_axioms prep_stmt prep_att raw_decls raw_fixes raw_prems raw_concls thy =
   let
     (*specification*)
-    val ((vars, [prems, concls], _, _), vars_ctxt) =
+    val ((vars, [prems, concls], _, _, _), vars_ctxt) =
       Proof_Context.init_global thy
       |> prep_stmt (raw_decls @ raw_fixes) ((map o map) (rpair []) [raw_prems, map snd raw_concls]);
     val (decls, fixes) = chop (length raw_decls) vars;