proper export of result_text for 'have';

--- a/src/Pure/Isar/proof.ML	Wed Sep 18 20:53:53 2019 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Sep 18 21:35:21 2019 +0200
@@ -1057,9 +1057,11 @@
         (if strict_asm then Assumption.assume_export else Assumption.presume_export);
 
     (*params*)
-    val ((params, assumes_propss, shows_propss, result_binds, result_text), params_ctxt) = ctxt
+    val ((params, assumes_propss, shows_propss, result_binds, text), params_ctxt) = ctxt
       |> prep_statement raw_fixes (map snd raw_assumes) (map snd raw_shows);
 
+    val result_text = singleton (Variable.export_terms params_ctxt ctxt) text;
+
     (*prems*)
     val (assumes_bindings, shows_bindings) =
       apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);