# HG changeset patch # User wenzelm # Date 1568830215 -7200 # Node ID c92d2abcc998fd10c7258463a6281fd99a2f21e6 # Parent d5559011b9e6b59fd6ca87c6c54b6004242a5d24 more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal); diff -r d5559011b9e6 -r c92d2abcc998 src/HOL/Eisbach/Tests.thy --- 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 \ C \ A \ B \ A \ C \ D \ True \ C" by (((match premises in I: "P \ Q" (cut) diff -r d5559011b9e6 -r c92d2abcc998 src/Pure/Isar/obtain.ML --- 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; diff -r d5559011b9e6 -r c92d2abcc998 src/Pure/Isar/proof.ML --- 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) diff -r d5559011b9e6 -r c92d2abcc998 src/Pure/Isar/proof_context.ML --- 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 diff -r d5559011b9e6 -r c92d2abcc998 src/Pure/Isar/specification.ML --- 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;