# HG changeset patch
# User wenzelm
# Date 1565637760 -7200
# Node ID 67580f2ded908d146f3b8d9a9da4eeb828834c36
# Parent  8d4abdbc6de9cd82e7f87cff2cee9f4a38d02f04# Parent  bf5724694ce5248610f01bcb44b3b6880ded0736
merged

diff -r 8d4abdbc6de9 -r 67580f2ded90 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon Aug 12 15:57:40 2019 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Mon Aug 12 21:22:40 2019 +0200
@@ -23,8 +23,6 @@
 structure Meson_Clausify : MESON_CLAUSIFY =
 struct
 
-open Meson
-
 (* the extra "Meson" helps prevent clashes (FIXME) *)
 val new_skolem_var_prefix = "MesonSK"
 val new_nonskolem_var_prefix = "MesonV"
@@ -306,14 +304,14 @@
          |> new_skolem ? forall_intr_vars
     val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
     val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
-                |> cong_extensionalize_thm ctxt
-                |> abs_extensionalize_thm ctxt
-                |> make_nnf ctxt
+                |> Meson.cong_extensionalize_thm ctxt
+                |> Meson.abs_extensionalize_thm ctxt
+                |> Meson.make_nnf ctxt
   in
     if new_skolem then
       let
         fun skolemize choice_ths =
-          skolemize_with_choice_theorems ctxt choice_ths
+          Meson.skolemize_with_choice_theorems ctxt choice_ths
           #> simplify (ss_only @{thms all_simps[symmetric]} ctxt)
         val no_choice = null choice_ths
         val pull_out =
@@ -323,7 +321,7 @@
             skolemize choice_ths
         val discharger_th = th |> pull_out
         val discharger_th =
-          discharger_th |> has_too_many_clauses ctxt (Thm.concl_of discharger_th)
+          discharger_th |> Meson.has_too_many_clauses ctxt (Thm.concl_of discharger_th)
                            ? (to_definitional_cnf_with_quantifiers ctxt
                               #> pull_out)
         val zapped_th =
@@ -356,18 +354,18 @@
          (NONE, (th, ctxt))
       end
     else
-      (NONE, (th |> has_too_many_clauses ctxt (Thm.concl_of th)
+      (NONE, (th |> Meson.has_too_many_clauses ctxt (Thm.concl_of th)
                     ? to_definitional_cnf_with_quantifiers ctxt, ctxt))
   end
 
 (* Convert a theorem to CNF, with additional premises due to skolemization. *)
 fun cnf_axiom ctxt0 new_skolem combinators ax_no th =
   let
-    val choice_ths = choice_theorems (Proof_Context.theory_of ctxt0)
+    val choice_ths = Meson.choice_theorems (Proof_Context.theory_of ctxt0)
     val (opt, (nnf_th, ctxt1)) =
       nnf_axiom choice_ths new_skolem ax_no th ctxt0
     fun clausify th =
-      make_cnf
+      Meson.make_cnf
        (if new_skolem orelse null choice_ths then []
         else map (old_skolem_theorem_of_def ctxt1) (old_skolem_defs th))
        th ctxt1
@@ -383,7 +381,7 @@
      cnf_ths |> map (combinators ? introduce_combinators_in_theorem ctxt2
                      #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
              |> Variable.export ctxt2 ctxt0
-             |> finish_cnf
+             |> Meson.finish_cnf
              |> map (Thm.close_derivation \<^here>))
   end
   handle THM _ => (NONE, [])
diff -r 8d4abdbc6de9 -r 67580f2ded90 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Aug 12 15:57:40 2019 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Aug 12 21:22:40 2019 +0200
@@ -41,11 +41,10 @@
   | _ => (s, false))
 
 fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) =
-    let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in
-      ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev)
-    end
+      let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s)
+      in ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev) end
   | atp_term_of_metis _ (Metis_Term.Var s) =
-    ATerm ((Metis_Name.toString s, []), [])
+      ATerm ((Metis_Name.toString s, []), [])
 
 fun hol_term_of_metis ctxt type_enc sym_tab =
   atp_term_of_metis type_enc #> term_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab NONE
@@ -80,43 +79,42 @@
                             " of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts'
   in ts' end
 
-(* ------------------------------------------------------------------------- *)
-(* FOL step Inference Rules                                                  *)
-(* ------------------------------------------------------------------------- *)
+
+
+(** FOL step Inference Rules **)
 
-fun lookth th_pairs fth =
-  the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
-  handle Option.Option => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
+fun lookth th_pairs fol_th =
+  (case AList.lookup (uncurry Metis_Thm.equal) th_pairs fol_th of
+    SOME th => th
+  | NONE => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fol_th))
 
 fun cterm_incr_types ctxt idx =
   Thm.cterm_of ctxt o map_types (Logic.incr_tvar idx)
 
+
 (* INFERENCE RULE: AXIOM *)
 
-(* This causes variables to have an index of 1 by default. See also
-   "term_of_atp" in "ATP_Proof_Reconstruct". *)
+(*This causes variables to have an index of 1 by default. See also
+  "term_of_atp" in "ATP_Proof_Reconstruct".*)
 val axiom_inference = Thm.incr_indexes 1 oo lookth
 
+
 (* INFERENCE RULE: ASSUME *)
 
-val EXCLUDED_MIDDLE = @{lemma "P \<Longrightarrow> \<not> P \<Longrightarrow> False" by (rule notE)}
-
-fun inst_excluded_middle ctxt i_atom =
-  let
-    val th = EXCLUDED_MIDDLE
-    val [vx] = Term.add_vars (Thm.prop_of th) []
-  in
-    infer_instantiate_types ctxt [(vx, Thm.cterm_of ctxt i_atom)] th
-  end
+fun inst_excluded_middle i_atom =
+  @{lemma "P \<Longrightarrow> \<not> P \<Longrightarrow> False" by (rule notE)}
+  |> instantiate_normalize ([], [((("P", 0), \<^typ>\<open>bool\<close>), i_atom)])
 
 fun assume_inference ctxt type_enc concealed sym_tab atom =
-  inst_excluded_middle ctxt
-    (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom))
+  singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)
+  |> Thm.cterm_of ctxt |> inst_excluded_middle
+
 
-(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
-   to reconstruct them admits new possibilities of errors, e.g. concerning
-   sorts. Instead we try to arrange that new TVars are distinct and that types
-   can be inferred from terms. *)
+(* INFERENCE RULE: INSTANTIATE (SUBST). *)
+
+(*Type instantiations are ignored. Trying to reconstruct them admits new
+  possibilities of errors, e.g. concerning sorts. Instead we try to arrange
+  hat new TVars are distinct and that types can be inferred from terms.*)
 
 fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
   let
@@ -127,7 +125,7 @@
     fun subst_translation (x,y) =
       let
         val v = find_var x
-        (* We call "polish_hol_terms" below. *)
+        (*We call "polish_hol_terms" below.*)
         val t = hol_term_of_metis ctxt type_enc sym_tab y
       in
         SOME (Thm.cterm_of ctxt (Var v), t)
@@ -146,15 +144,15 @@
           SOME b => SOME (b, t)
         | NONE =>
           (case unprefix_and_unascii tvar_prefix a of
-            SOME _ => NONE (* type instantiations are forbidden *)
-          | NONE => SOME (a, t) (* internal Metis var? *)))
+            SOME _ => NONE (*type instantiations are forbidden*)
+          | NONE => SOME (a, t) (*internal Metis var?*)))
       end
     val _ = trace_msg ctxt (fn () => "  isa th: " ^ Thm.string_of_thm ctxt i_th)
     val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
     val (vars, tms) =
       ListPair.unzip (map_filter subst_translation substs)
       ||> polish_hol_terms ctxt concealed
-    val ctm_of = cterm_incr_types ctxt (1 + Thm.maxidx_of i_th)
+    val ctm_of = cterm_incr_types ctxt (Thm.maxidx_of i_th + 1)
     val substs' = ListPair.zip (vars, map ctm_of tms)
     val _ = trace_msg ctxt (fn () =>
       cat_lines ("subst_translations:" ::
@@ -167,6 +165,7 @@
   handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg)
        | ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg)
 
+
 (* INFERENCE RULE: RESOLVE *)
 
 (*Increment the indexes of only the type variables*)
@@ -178,15 +177,15 @@
     Thm.instantiate (map inc_tvar tvs, []) th
   end
 
-(* Like RSN, but we rename apart only the type variables. Vars here typically
-   have an index of 1, and the use of RSN would increase this typically to 3.
-   Instantiations of those Vars could then fail. *)
-fun resolve_inc_tyvars ctxt tha i thb =
+(*Like RSN, but we rename apart only the type variables. Vars here typically
+  have an index of 1, and the use of RSN would increase this typically to 3.
+  Instantiations of those Vars could then fail.*)
+fun resolve_inc_tyvars ctxt th1 i th2 =
   let
-    val tha = incr_type_indexes ctxt (1 + Thm.maxidx_of thb) tha
+    val th1' = incr_type_indexes ctxt (Thm.maxidx_of th2 + 1) th1
     fun res (tha, thb) =
       (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
-            (false, tha, Thm.nprems_of tha) i thb
+            (false, Thm.close_derivation \<^here> tha, Thm.nprems_of tha) i thb
            |> Seq.list_of |> distinct Thm.eq_thm of
         [th] => th
       | _ =>
@@ -200,11 +199,11 @@
             res (tha', thb')
         end)
   in
-    res (tha, thb)
+    res (th1', th2)
     handle TERM z =>
       let
         val ps = []
-          |> fold (Term.add_vars o Thm.prop_of) [tha, thb]
+          |> fold (Term.add_vars o Thm.prop_of) [th1', th2]
           |> AList.group (op =)
           |> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts)
           |> rpair Envir.init
@@ -212,13 +211,13 @@
           |> Envir.type_env |> Vartab.dest
           |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T))
       in
-        (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
-           "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
-           first argument). We then perform unification of the types of variables by hand and try
-           again. We could do this the first time around but this error occurs seldom and we don't
-           want to break existing proofs in subtle ways or slow them down. *)
+        (*The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
+          "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
+          first argument). We then perform unification of the types of variables by hand and try
+          again. We could do this the first time around but this error occurs seldom and we don't
+          want to break existing proofs in subtle ways or slow them down.*)
         if null ps then raise TERM z
-        else res (apply2 (Drule.instantiate_normalize (ps, [])) (tha, thb))
+        else res (apply2 (Drule.instantiate_normalize (ps, [])) (th1', th2))
       end
   end
 
@@ -230,8 +229,8 @@
 
 val normalize_literal = simp_not_not o Envir.eta_contract
 
-(* Find the relative location of an untyped term within a list of terms as a
-   1-based index. Returns 0 in case of failure. *)
+(*Find the relative location of an untyped term within a list of terms as a
+  1-based index. Returns 0 in case of failure.*)
 fun index_of_literal lit haystack =
   let
     fun match_lit normalize =
@@ -243,18 +242,18 @@
      | j => j) + 1
   end
 
-(* Permute a rule's premises to move the i-th premise to the last position. *)
+(*Permute a rule's premises to move the i-th premise to the last position.*)
 fun make_last i th =
   let val n = Thm.nprems_of th in
     if i >= 1 andalso i <= n then Thm.permute_prems (i - 1) 1 th
     else raise THM ("select_literal", i, [th])
   end
 
-(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
-   to create double negations. The "select" wrapper is a trick to ensure that
-   "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
-   don't use this trick in general because it makes the proof object uglier than
-   necessary. FIXME. *)
+(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
+  to create double negations. The "select" wrapper is a trick to ensure that
+  "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
+  don't use this trick in general because it makes the proof object uglier than
+  necessary. FIXME.*)
 fun negate_head ctxt th =
   if exists (fn t => t aconv \<^prop>\<open>\<not> False\<close>) (Thm.prems_of th) then
     (th RS @{thm select_FalseI})
@@ -296,41 +295,41 @@
       end
   end
 
+
 (* INFERENCE RULE: REFL *)
 
-val REFL_THM = Thm.incr_indexes 2 @{lemma "t \<noteq> t \<Longrightarrow> False" by (drule notE) (rule refl)}
-
+val REFL_THM = Thm.incr_indexes 2 @{lemma "x \<noteq> x \<Longrightarrow> False" by (drule notE) (rule refl)}
 val [refl_x] = Term.add_vars (Thm.prop_of REFL_THM) [];
-val refl_idx = 1 + Thm.maxidx_of REFL_THM;
 
 fun refl_inference ctxt type_enc concealed sym_tab t =
   let
     val i_t = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
     val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
-    val c_t = cterm_incr_types ctxt refl_idx i_t
+    val c_t = cterm_incr_types ctxt (Thm.maxidx_of REFL_THM + 1) i_t
   in infer_instantiate_types ctxt [(refl_x, c_t)] REFL_THM end
 
+
 (* INFERENCE RULE: EQUALITY *)
 
 val subst_em = @{lemma "s = t \<Longrightarrow> P s \<Longrightarrow> \<not> P t \<Longrightarrow> False" by (erule notE) (erule subst)}
 val ssubst_em = @{lemma "s = t \<Longrightarrow> P t \<Longrightarrow> \<not> P s \<Longrightarrow> False" by (erule notE) (erule ssubst)}
 
 fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr =
-  let val thy = Proof_Context.theory_of ctxt
-      val m_tm = Metis_Term.Fn atom
-      val [i_atom, i_tm] = hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr]
-      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
-      fun replace_item_list lx 0 (_::ls) = lx::ls
-        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
-      fun path_finder_fail tm ps t =
-        raise METIS_RECONSTRUCT ("equality_inference (path_finder)",
-                  "path = " ^ space_implode " " (map string_of_int ps) ^
-                  " isa-term: " ^ Syntax.string_of_term ctxt tm ^
-                  (case t of
-                    SOME t => " fol-term: " ^ Metis_Term.toString t
-                  | NONE => ""))
-      fun path_finder tm [] _ = (tm, Bound 0)
-        | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
+  let
+    val m_tm = Metis_Term.Fn atom
+    val [i_atom, i_tm] = hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr]
+    val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
+    fun replace_item_list lx 0 (_::ls) = lx::ls
+      | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
+    fun path_finder_fail tm ps t =
+      raise METIS_RECONSTRUCT ("equality_inference (path_finder)",
+                "path = " ^ space_implode " " (map string_of_int ps) ^
+                " isa-term: " ^ Syntax.string_of_term ctxt tm ^
+                (case t of
+                  SOME t => " fol-term: " ^ Metis_Term.toString t
+                | NONE => ""))
+    fun path_finder tm [] _ = (tm, Bound 0)
+      | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
           let
             val s = s |> Metis_Name.toString
                       |> perhaps (try (unprefix_and_unascii const_prefix
@@ -361,35 +360,38 @@
                 val (r, t) = path_finder tm_p ps (nth ts p)
               in (r, list_comb (tm1, replace_item_list t p' args)) end
           end
-        | path_finder tm ps t = path_finder_fail tm ps (SOME t)
-      val (tm_subst, body) = path_finder i_atom fp m_tm
-      val tm_abs = Abs ("x", type_of tm_subst, body)
-      val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
-      val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
-      val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
-      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill-typed but gives right max*)
-      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
-      val _ = trace_msg ctxt (fn () => "subst' " ^ Thm.string_of_thm ctxt subst')
-      val eq_terms =
-        map (apply2 (Thm.cterm_of ctxt))
-          (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm]))
+      | path_finder tm ps t = path_finder_fail tm ps (SOME t)
+    val (tm_subst, body) = path_finder i_atom fp m_tm
+    val tm_abs = Abs ("x", type_of tm_subst, body)
+    val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
+    val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
+    val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
+    val maxidx = fold Term.maxidx_term [i_tm, tm_abs, tm_subst] ~1
+    val subst' = Thm.incr_indexes (maxidx + 1) (if pos then subst_em else ssubst_em)
+    val _ = trace_msg ctxt (fn () => "subst' " ^ Thm.string_of_thm ctxt subst')
+    val eq_terms =
+      map (apply2 (Thm.cterm_of ctxt))
+        (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm]))
   in
     infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) eq_terms) subst'
   end
 
 val factor = Seq.hd o distinct_subgoals_tac
 
-fun one_step ctxt type_enc concealed sym_tab th_pairs p =
-  (case p of
-    (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
-  | (_, Metis_Proof.Assume f_atom) => assume_inference ctxt type_enc concealed sym_tab f_atom
-  | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
-    inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1 |> factor
-  | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
-    resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1 f_th2 |> factor
-  | (_, Metis_Proof.Refl f_tm) => refl_inference ctxt type_enc concealed sym_tab f_tm
-  | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
-    equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r)
+fun one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inference) =
+  (case inference of
+    Metis_Proof.Axiom _ =>
+      axiom_inference th_pairs fol_th |> factor
+  | Metis_Proof.Assume atom =>
+      assume_inference ctxt type_enc concealed sym_tab atom
+  | Metis_Proof.Metis_Subst (subst, th1) =>
+      inst_inference ctxt type_enc concealed sym_tab th_pairs subst th1 |> factor
+  | Metis_Proof.Resolve (atom, th1, th2) =>
+      resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 |> factor
+  | Metis_Proof.Refl tm =>
+      refl_inference ctxt type_enc concealed sym_tab tm
+  | Metis_Proof.Equality (lit, p, r) =>
+      equality_inference ctxt type_enc concealed sym_tab lit p r)
 
 fun flexflex_first_order ctxt th =
   (case Thm.tpairs_of th of
@@ -398,10 +400,10 @@
       let
         val thy = Proof_Context.theory_of ctxt
         val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
-  
+
         fun mkT (v, (S, T)) = ((v, S), Thm.ctyp_of ctxt T)
         fun mk (v, (T, t)) = ((v, Envir.subst_type tyenv T), Thm.cterm_of ctxt t)
-  
+
         val instsT = Vartab.fold (cons o mkT) tyenv []
         val insts = Vartab.fold (cons o mk) tenv []
       in
@@ -416,10 +418,10 @@
 
 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
 
-(* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
-   disjuncts are impossible. In the Isabelle proof, in spite of efforts to
-   eliminate them, duplicates sometimes appear with slightly different (but
-   unifiable) types. *)
+(*Seldomly needed hack. A Metis clause is represented as a set, so duplicate
+  disjuncts are impossible. In the Isabelle proof, in spite of efforts to
+  eliminate them, duplicates sometimes appear with slightly different (but
+  unifiable) types.*)
 fun resynchronize ctxt fol_th th =
   let
     val num_metis_lits =
@@ -447,12 +449,11 @@
       end
   end
 
-fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf)
-                         th_pairs =
+fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf) th_pairs =
   if not (null th_pairs) andalso Thm.prop_of (snd (hd th_pairs)) aconv \<^prop>\<open>False\<close> then
-    (* Isabelle sometimes identifies literals (premises) that are distinct in
-       Metis (e.g., because of type variables). We give the Isabelle proof the
-       benefice of the doubt. *)
+    (*Isabelle sometimes identifies literals (premises) that are distinct in
+      Metis (e.g., because of type variables). We give the Isabelle proof the
+      benefice of the doubt.*)
     th_pairs
   else
     let
@@ -468,12 +469,12 @@
       (fol_th, th) :: th_pairs
     end
 
-(* It is normally sufficient to apply "assume_tac" to unify the conclusion with
-   one of the premises. Unfortunately, this sometimes yields "Variable
-   has two distinct types" errors. To avoid this, we instantiate the
-   variables before applying "assume_tac". Typical constraints are of the form
-     ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z \<equiv>\<^sup>? SK_a_b_c_x,
-   where the nonvariables are goal parameters. *)
+(*It is normally sufficient to apply "assume_tac" to unify the conclusion with
+  one of the premises. Unfortunately, this sometimes yields "Variable
+  has two distinct types" errors. To avoid this, we instantiate the
+  variables before applying "assume_tac". Typical constraints are of the form
+    ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z \<equiv>\<^sup>? SK_a_b_c_x,
+  where the nonvariables are goal parameters.*)
 fun unify_first_prem_with_concl ctxt i th =
   let
     val goal = Logic.get_goal (Thm.prop_of th) i |> Envir.beta_eta_contract
@@ -523,15 +524,15 @@
     infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) t_inst) th
   end
 
-val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by assumption}
+val copy_prem = @{lemma "P \<Longrightarrow> (P \<Longrightarrow> P \<Longrightarrow> Q) \<Longrightarrow> Q" by assumption}
 
 fun copy_prems_tac ctxt [] ns i =
-    if forall (curry (op =) 1) ns then all_tac else copy_prems_tac ctxt (rev ns) [] i
+      if forall (curry (op =) 1) ns then all_tac else copy_prems_tac ctxt (rev ns) [] i
   | copy_prems_tac ctxt (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ctxt ms (1 :: ns) i
   | copy_prems_tac ctxt (m :: ms) ns i =
-    eresolve_tac ctxt [copy_prem] i THEN copy_prems_tac ctxt ms (m div 2 :: (m + 1) div 2 :: ns) i
+      eresolve_tac ctxt [copy_prem] i THEN copy_prems_tac ctxt ms (m div 2 :: (m + 1) div 2 :: ns) i
 
-(* Metis generates variables of the form _nnn. *)
+(*Metis generates variables of the form _nnn.*)
 val is_metis_fresh_variable = String.isPrefix "_"
 
 fun instantiate_forall_tac ctxt t i st =
@@ -539,16 +540,16 @@
     val params = Logic.strip_params (Logic.get_goal (Thm.prop_of st) i) |> rev
 
     fun repair (t as (Var ((s, _), _))) =
-        (case find_index (fn (s', _) => s' = s) params of
-          ~1 => t
-        | j => Bound j)
+          (case find_index (fn (s', _) => s' = s) params of
+            ~1 => t
+          | j => Bound j)
       | repair (t $ u) =
-        (case (repair t, repair u) of
-          (t as Bound j, u as Bound k) =>
-          (* This is a trick to repair the discrepancy between the fully skolemized term that MESON
-             gives us (where existentials were pulled out) and the reality. *)
-          if k > j then t else t $ u
-        | (t, u) => t $ u)
+          (case (repair t, repair u) of
+            (t as Bound j, u as Bound k) =>
+            (*This is a trick to repair the discrepancy between the fully skolemized term that MESON
+              gives us (where existentials were pulled out) and the reality.*)
+            if k > j then t else t $ u
+          | (t, u) => t $ u)
       | repair t = t
 
     val t' = t |> repair |> fold (absdummy o snd) params
@@ -618,23 +619,26 @@
 val tysubst_ord =
   list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
 
-structure Int_Tysubst_Table =
-  Table(type key = int * (indexname * (sort * typ)) list
-        val ord = prod_ord int_ord tysubst_ord)
+structure Int_Tysubst_Table = Table
+(
+  type key = int * (indexname * (sort * typ)) list
+  val ord = prod_ord int_ord tysubst_ord
+)
 
-structure Int_Pair_Graph =
-  Graph(type key = int * int val ord = prod_ord int_ord int_ord)
+structure Int_Pair_Graph = Graph(
+  type key = int * int
+  val ord = prod_ord int_ord int_ord
+)
 
 fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
 fun shuffle_ord p = prod_ord int_ord int_ord (apply2 shuffle_key p)
 
-(* Attempts to derive the theorem "False" from a theorem of the form
-   "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
-   specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
-   must be eliminated first. *)
+(*Attempts to derive the theorem "False" from a theorem of the form
+  "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
+  specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
+  must be eliminated first.*)
 fun discharge_skolem_premises ctxt axioms prems_imp_false =
-  if Thm.prop_of prems_imp_false aconv \<^prop>\<open>False\<close> then
-    prems_imp_false
+  if Thm.prop_of prems_imp_false aconv \<^prop>\<open>False\<close> then prems_imp_false
   else
     let
       val thy = Proof_Context.theory_of ctxt
diff -r 8d4abdbc6de9 -r 67580f2ded90 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Aug 12 15:57:40 2019 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Aug 12 21:22:40 2019 +0200
@@ -176,7 +176,8 @@
       | get_isa_thm mth Isa_Lambda_Lifted =
           lam_lifted_of_metis ctxt type_enc sym_tab concealed mth
       | get_isa_thm _ (Isa_Raw ith) = ith
-    val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
+    val axioms = axioms |> map (fn (mth, ith) =>
+      (mth, get_isa_thm mth ith |> Thm.close_derivation \<^here>))
     val _ = trace_msg ctxt (K "ISABELLE CLAUSES")
     val _ = List.app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms
     val _ = trace_msg ctxt (K "METIS CLAUSES")
@@ -208,15 +209,12 @@
             val used = map_filter (used_axioms axioms) proof
             val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
             val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used
-            val (used_th_cls_pairs, unused_th_cls_pairs) =
-              List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs
-            val unused_ths = maps (snd o snd) unused_th_cls_pairs
-            val unused_names = map fst unused_th_cls_pairs
 
-            val _ = unused := unused_ths;
+            val unused_th_cls_pairs = filter_out (have_common_thm ctxt used o #2 o #2) th_cls_pairs
+            val _ = unused := maps (#2 o #2) unused_th_cls_pairs;
             val _ =
-              if not (null unused_names) then
-                verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused_names)
+              if not (null unused_th_cls_pairs) then
+                verbose_warning ctxt ("Unused theorems: " ^ commas_quote (map #1 unused_th_cls_pairs))
               else ();
             val _ =
               if not (null cls) andalso not (have_common_thm ctxt used cls) then
diff -r 8d4abdbc6de9 -r 67580f2ded90 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Aug 12 15:57:40 2019 +0200
+++ b/src/Pure/Tools/build.scala	Mon Aug 12 21:22:40 2019 +0200
@@ -289,6 +289,7 @@
             }
 
           process.result(
+            progress_stderr = Output.writeln(_),
             progress_stdout = (line: String) =>
               Library.try_unprefix("\floading_theory = ", line) match {
                 case Some(theory) =>
diff -r 8d4abdbc6de9 -r 67580f2ded90 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Aug 12 15:57:40 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Aug 12 21:22:40 2019 +0200
@@ -821,42 +821,34 @@
   let val U = Term.itselfT T --> propT
   in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
 
+fun term_of _ (PThm ({name, types = Ts, ...}, _)) =
+      fold AppT (these Ts) (Const (Long_Name.append "thm" name, proofT))
+  | term_of _ (PAxm (name, _, Ts)) =
+      fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
+  | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
+  | term_of _ (PBound i) = Bound i
+  | term_of Ts (Abst (s, opT, prf)) =
+      let val T = the_default dummyT opT in
+        Const ("Pure.Abst", (T --> proofT) --> proofT) $
+          Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
+      end
+  | term_of Ts (AbsP (s, t, prf)) =
+      AbsPt $ the_default Term.dummy_prop t $
+        Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
+  | term_of Ts (prf1 %% prf2) =
+      AppPt $ term_of Ts prf1 $ term_of Ts prf2
+  | term_of Ts (prf % opt) =
+      let
+        val t = the_default Term.dummy opt;
+        val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
+      in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
+  | term_of _ (Hyp t) = Hypt $ t
+  | term_of _ (Oracle (_, t, _)) = Oraclet $ t
+  | term_of _ MinProof = MinProoft;
+
 in
 
-fun thm_const_default (_: proof_serial) name = Long_Name.append "thm" name;
-fun axm_const_default name = Long_Name.append "axm" name;
-
-fun term_of
-   {thm_const: proof_serial -> string -> string,
-    axm_const: string -> string} =
-  let
-    fun term _ (PThm ({serial = i, name, types = Ts, ...}, _)) =
-          fold AppT (these Ts) (Const (thm_const i name, proofT))
-      | term _ (PAxm (name, _, Ts)) =
-          fold AppT (these Ts) (Const (axm_const name, proofT))
-      | term _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
-      | term _ (PBound i) = Bound i
-      | term Ts (Abst (s, opT, prf)) =
-          let val T = the_default dummyT opT in
-            Const ("Pure.Abst", (T --> proofT) --> proofT) $
-              Abs (s, T, term (T::Ts) (incr_pboundvars 1 0 prf))
-          end
-      | term Ts (AbsP (s, t, prf)) =
-          AbsPt $ the_default Term.dummy_prop t $
-            Abs (s, proofT, term (proofT::Ts) (incr_pboundvars 0 1 prf))
-      | term Ts (prf1 %% prf2) =
-          AppPt $ term Ts prf1 $ term Ts prf2
-      | term Ts (prf % opt) =
-          let
-            val t = the_default Term.dummy opt;
-            val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
-          in Const ("Pure.Appt", proofT --> T --> proofT) $ term Ts prf $ t end
-      | term _ (Hyp t) = Hypt $ t
-      | term _ (Oracle (_, t, _)) = Oraclet $ t
-      | term _ MinProof = MinProoft;
-  in term [] end;
-
-val term_of_proof = term_of {thm_const = thm_const_default, axm_const = axm_const_default};
+val term_of_proof = term_of [];
 
 end;
 
@@ -2009,12 +2001,29 @@
 
 fun clean_proof thy = rew_proof thy #> shrink_proof;
 
+
+local open XML.Encode Term_XML.Encode in
+
+fun proof prf = prf |> variant
+ [fn MinProof => ([], []),
+  fn PBound a => ([int_atom a], []),
+  fn Abst (a, SOME b, c) => ([a], pair typ proof (b, c)),
+  fn AbsP (a, SOME b, c) => ([a], pair term proof (b, c)),
+  fn a % SOME b => ([], pair proof term (a, b)),
+  fn a %% b => ([], pair proof proof (a, b)),
+  fn Hyp a => ([], term a),
+  fn PAxm (name, b, SOME Ts) => ([name], list typ Ts),
+  fn OfClass (T, c) => ([c], typ T),
+  fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
+  fn PThm ({serial, name, types = SOME Ts, ...}, _) => ([int_atom serial, name], list typ Ts)];
+
+fun encode_export prop prf = pair term proof (prop, prf);
+
+end;
+
 fun export_proof thy i prop prf =
   let
-    val xml =
-      reconstruct_proof thy prop prf
-      |> term_of {thm_const = K o string_of_int, axm_const = axm_const_default}
-      |> Term_XML.Encode.term;
+    val xml = reconstruct_proof thy prop prf |> encode_export prop;
     val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
   in
     chunks |> Export.export_params
diff -r 8d4abdbc6de9 -r 67580f2ded90 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Aug 12 15:57:40 2019 +0200
+++ b/src/Pure/thm.ML	Mon Aug 12 21:22:40 2019 +0200
@@ -1007,8 +1007,7 @@
       val Deriv {promises, body} = der;
       val {shyps, hyps, prop, tpairs, ...} = args;
 
-      fun err msg = raise THM ("name_derivation: " ^ msg, 0, [thm]);
-      val _ = null tpairs orelse err "bad flex-flex constraints";
+      val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]);
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
       val (pthm, proof) =
@@ -1019,7 +1018,8 @@
 
 fun close_derivation pos =
   solve_constraints #> (fn thm =>
-    if derivation_closed thm then thm else name_derivation ("", pos) thm);
+    if not (null (tpairs_of thm)) orelse derivation_closed thm then thm
+    else name_derivation ("", pos) thm);
 
 val trim_context = solve_constraints #> trim_context_thm;