# HG changeset patch
# User wenzelm
# Date 1568898552 -7200
# Node ID 31364e70ff3e45eec9b59bfa306ee4f402623419
# Parent  ce1afe0f3071dfc2e11f59b8216d74c334a31292
clarified signature;

diff -r ce1afe0f3071 -r 31364e70ff3e src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Sep 19 10:52:18 2019 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Sep 19 15:09:12 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, result_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;
@@ -230,7 +230,7 @@
       [((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
       [(Binding.empty_atts, [(thesis, [])])] int
     |-> Proof.refine_insert
-    |> Proof.map_context (fold Variable.bind_term binds')
+    |> Proof.map_context (fold Variable.bind_term result_binds)
   end;
 
 in
diff -r ce1afe0f3071 -r 31364e70ff3e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Sep 19 10:52:18 2019 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Sep 19 15:09:12 2019 +0200
@@ -645,8 +645,8 @@
     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, text), _) =
-      prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt;
+    val {fixes = params, assumes = prems_propss, shows = concl_propss, result_binds, text, ...} =
+      #1 (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
     state
@@ -812,7 +812,7 @@
     val ctxt = context_of state;
 
     (*vars*)
-    val ((vars, propss, _, binds', _), vars_ctxt) =
+    val ({vars, propss, result_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;
@@ -846,7 +846,7 @@
         raw_defs def_thmss;
   in
     state
-    |> map_context (K defs_ctxt #> fold Variable.bind_term binds')
+    |> map_context (K defs_ctxt #> fold Variable.bind_term result_binds)
     |> note_thmss notes
   end;
 
@@ -1057,11 +1057,10 @@
         (if strict_asm then Assumption.assume_export else Assumption.presume_export);
 
     (*params*)
-    val ((params, assumes_propss, shows_propss, result_binds, text), params_ctxt) = ctxt
+    val ({fixes = params, assumes = assumes_propss, shows = shows_propss,
+          result_binds, result_text, 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);
diff -r ce1afe0f3071 -r 31364e70ff3e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Sep 19 10:52:18 2019 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Sep 19 15:09:12 2019 +0200
@@ -169,22 +169,28 @@
   val generic_add_abbrev: string -> binding * term -> Context.generic ->
     (term * term) * Context.generic
   val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
-  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 * 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 * term) * Proof.context
+  type stmt =
+   {vars: ((binding * typ option * mixfix) * (string * term)) list,
+    propss: term list list,
+    binds: (indexname * term) list,
+    result_binds: (indexname * term) list}
+  val cert_stmt: (binding * typ option * mixfix) list -> (term * term list) list list ->
+    Proof.context -> stmt * Proof.context
+  val read_stmt: (binding * string option * mixfix) list -> (string * string list) list list ->
+    Proof.context -> stmt * Proof.context
+  type statement =
+   {fixes: (string * term) list,
+    assumes: term list list,
+    shows: term list list,
+    result_binds: (indexname * term option) list,
+    text: term,
+    result_text: term}
   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 * term) *
-      Proof.context
+    statement * 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 * term) *
-      Proof.context
+    statement * Proof.context
   val print_syntax: Proof.context -> unit
   val print_abbrevs: bool -> Proof.context -> unit
   val pretty_term_bindings: Proof.context -> Pretty.T list
@@ -1334,6 +1340,20 @@
 
 (* structured statements *)
 
+type stmt =
+ {vars: ((binding * typ option * mixfix) * (string * term)) list,
+  propss: term list list,
+  binds: (indexname * term) list,
+  result_binds: (indexname * term) list};
+
+type statement =
+ {fixes: (string * term) list,
+  assumes: term list list,
+  shows: term list list,
+  result_binds: (indexname * term option) list,
+  text: term,
+  result_text: term};
+
 local
 
 fun export_binds ctxt' ctxt params binds =
@@ -1362,25 +1382,36 @@
       |> export_binds params_ctxt ctxt params
       |> map (apsnd the);
 
-    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;
+    val result : stmt =
+      {vars = vars' ~~ params, propss = propss, binds = binds, result_binds = binds'};
+  in (result, params_ctxt) end;
 
 fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
   let
-    val ((fixes, (assumes, shows), binds, text'), ctxt') = ctxt
+    val ((fixes, (assumes, shows), binds), ctxt') = ctxt
       |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows)
-      |-> (fn (vars, propss, binds, _, text') =>
+      |-> (fn {vars, propss, binds, ...} =>
         fold Variable.bind_term binds #>
-        pair (map #2 vars, chop (length raw_assumes) propss, binds, text'));
+        pair (map #2 vars, chop (length raw_assumes) propss, binds));
     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', text'), ctxt') end;
+
+    val text = Logic.close_prop fixes (flat assumes) (Logic.mk_conjunction_list (flat shows));
+    val text' = singleton (Variable.export_terms ctxt' ctxt) text;
+
+    val result : statement =
+     {fixes = fixes,
+      assumes = assumes,
+      shows = shows,
+      result_binds = binds',
+      text = text,
+      result_text = text'};
+  in (result, ctxt') end;
 
 in
 
diff -r ce1afe0f3071 -r 31364e70ff3e src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Sep 19 10:52:18 2019 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Sep 19 15:09:12 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, propss = [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;