support soft types for 'assume';
clarified "text": avoid polymorphism due to premature export;
--- 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;
--- 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;