src/HOL/Tools/Metis/metis_reconstruct.ML

   (case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
     SOME ((s, _), (_, swap)) => (s, swap)
   | _ => (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
 
 fun atp_literal_of_metis type_enc (pos, atom) =

     val _ = List.app (fn t => trace_msg ctxt
                   (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
                             " 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 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
+  let val [vx] = Term.add_vars (Thm.prop_of EXCLUDED_MIDDLE) []
+  in infer_instantiate_types ctxt [(vx, Thm.cterm_of ctxt i_atom)] EXCLUDED_MIDDLE end
 
 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))
 

 
     fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
     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)
       end
       handle Option.Option =>

       let val a = Metis_Name.toString a in
         (case unprefix_and_unascii schematic_var_prefix a of
           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)

     infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) substs') i_th
   end
   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*)
 fun incr_type_indexes ctxt inc th =
   let

     fun inc_tvar ((a, i), s) = (((a, i), s), Thm.ctyp_of ctxt (TVar ((a, i + inc), s)))
   in
     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. *)
+(*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 =
   let
     val tha = incr_type_indexes ctxt (1 + Thm.maxidx_of thb) tha
     fun res (tha, thb) =
       (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}

           |> rpair Envir.init
           |-> fold (Pattern.unify (Context.Proof ctxt))
           |> 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))
       end
   end
 

   | simp_not_not (\<^const>\<open>Not\<close> $ t) = s_not (simp_not_not t)
   | simp_not_not t = t
 
 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 =
       HOLogic.dest_Trueprop #> normalize
       #> curry Term.aconv_untyped (lit |> normalize)

     (case find_index (match_lit I) haystack of
        ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
      | 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})
     |> fold (rewrite_rule ctxt o single) @{thms not_atomize_select atomize_not_select}
   else

               resolve_inc_tyvars ctxt (select_literal ctxt j1 i_th1) j2 i_th2
               handle TERM (s, _) => raise METIS_RECONSTRUCT ("resolve_inference", s)))))
       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_x] = Term.add_vars (Thm.prop_of REFL_THM) [];

     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
   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
                                        #> the #> unmangled_const_name #> hd))
           in

                     "path_finder: " ^ string_of_int p ^ "  " ^
                     Syntax.string_of_term ctxt tm_p)
                 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 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]))
   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
+      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
+      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)
+      equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r)
 
 fun flexflex_first_order ctxt th =
   (case Thm.tpairs_of th of
     [] => th
   | pairs =>
       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
         Thm.instantiate (instsT, insts) th
       end

 fun is_isabelle_literal_genuine t =
   (case t of _ $ (Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _) => false | _ => true)
 
 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 =
       count is_metis_literal_genuine (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
     val num_isabelle_lits = count is_isabelle_literal_genuine (Thm.prems_of th)

           Goal.prove ctxt' [] [] goal (K tac)
           |> resynchronize ctxt' fol_th
       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
       val _ = trace_msg ctxt (fn () => "=============================================")
       val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)

       val _ = trace_msg ctxt (fn () => "=============================================")
     in
       (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
     val prem = goal |> Logic.strip_assums_hyp |> hd
     val concl = goal |> Logic.strip_assums_concl

          |> the_default [] (* FIXME *)
   in
     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
-
-(* Metis generates variables of the form _nnn. *)
+      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.*)
 val is_metis_fresh_variable = String.isPrefix "_"
 
 fun instantiate_forall_tac ctxt t i st =
   let
     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
 
     fun do_instantiate th =

   prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord)) (apply2 cluster_key p)
 
 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_Pair_Graph =
-  Graph(type key = int * int val ord = prod_ord int_ord int_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
+)
 
 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
 
       fun match_term p =