# HG changeset patch
# User wenzelm
# Date 1568839561 -7200
# Node ID 53fa2e4e79af7086d1b976bc8f024f30febbc37d
# Parent  5b86068ffc111ddd01017f11c9947487a077c68c
support soft types for 'have' etc., with careful export wrt. result text to avoid extra assumptions (details may differ due to polymorphism);

diff -r 5b86068ffc11 -r 53fa2e4e79af src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Sep 18 21:35:21 2019 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Sep 18 22:46:01 2019 +0200
@@ -1066,6 +1066,7 @@
     val (assumes_bindings, shows_bindings) =
       apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
     val (that_fact, goal_ctxt) = params_ctxt
+      |> fold Proof_Context.augment (text :: flat (assumes_propss @ shows_propss))
       |> fold_burrow add_assumes ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
       |> (fn (premss, ctxt') =>
           let
@@ -1085,13 +1086,13 @@
       let
         val ctxt' = context_of state';
         val export0 =
-          Assumption.export false result_ctxt ctxt' #>
+          Assumption.export false result_ctxt (Proof_Context.augment result_text ctxt') #>
           fold_rev (fn (x, v) => Thm.forall_intr_name (x, Thm.cterm_of params_ctxt v)) params #>
           Raw_Simplifier.norm_hhf_protect ctxt';
         val export = map export0 #> Variable.export result_ctxt ctxt';
       in
         state'
-        |> map_context (Variable.declare_term result_text)
+        |> map_context (Proof_Context.augment 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)