# HG changeset patch
# User wenzelm
# Date 1568832833 -7200
# Node ID 7b5ee1fa5029c7ae7659e55d5c07b241fb67c29a
# Parent  c92d2abcc998fd10c7258463a6281fd99a2f21e6
support soft types for 'assume';
clarified "text": avoid polymorphism due to premature export;

diff -r c92d2abcc998 -r 7b5ee1fa5029 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Sep 18 20:10:15 2019 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Sep 18 20:53:53 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, text), _) =
       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
@@ -653,7 +653,7 @@
     |> assert_forward
     |> map_context_result (fn ctxt =>
       ctxt
-      |> (fold o fold) Variable.declare_term propss
+      |> Proof_Context.augment text
       |> fold Variable.maybe_bind_term result_binds
       |> fold_burrow (Assumption.add_assms export o map (Thm.cterm_of ctxt)) propss
       |-> (fn premss =>
@@ -812,7 +812,7 @@
     val ctxt = context_of state;
 
     (*vars*)
-    val ((vars, propss, _, binds', text'), vars_ctxt) =
+    val ((vars, propss, _, binds', _), 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;
diff -r c92d2abcc998 -r 7b5ee1fa5029 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Sep 18 20:10:15 2019 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Sep 18 20:53:53 2019 +0200
@@ -1363,9 +1363,7 @@
       |> 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 text' = Logic.close_prop params [] (Logic.mk_conjunction_list (flat propss));
 
     val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt;
   in ((vars' ~~ params, propss, binds, binds', text'), params_ctxt) end;