src/HOL/Tools/metis_tools.ML

         val substs' = ListPair.zip (vars, map ctm_of tms)
         val _ = Output.debug (fn() => "subst_translations:")
         val _ = app (fn (x,y) => Output.debug (fn () => Display.string_of_cterm x ^ " |-> " ^
                                                         Display.string_of_cterm y))
                   substs'
-    in  cterm_instantiate substs' i_th  end;
+    in  cterm_instantiate substs' i_th  
+        handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
+    end;
 
   (* INFERENCE RULE: RESOLVE *)
 
   (*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

         val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm subst')
         val eq_terms = map (pairself (cterm_of thy))
                            (ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
     in  cterm_instantiate eq_terms subst'  end;
 
+  val factor = Seq.hd o distinct_subgoals_tac;
+
   fun step ctxt isFO thpairs (fol_th, Metis.Proof.Axiom _)                        =
-        axiom_inf ctxt thpairs fol_th
+        factor (axiom_inf ctxt thpairs fol_th)
     | step ctxt isFO thpairs (_, Metis.Proof.Assume f_atm)                        =
         assume_inf ctxt f_atm
-    | step ctxt isFO thpairs (_, Metis.Proof.Subst(f_subst, f_th1))                =
-        inst_inf ctxt thpairs f_subst f_th1
+    | step ctxt isFO thpairs (_, Metis.Proof.Subst(f_subst, f_th1))               =
+        factor (inst_inf ctxt thpairs f_subst f_th1)
     | step ctxt isFO thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2))        =
-        resolve_inf ctxt thpairs f_atm f_th1 f_th2
+        factor (resolve_inf ctxt thpairs f_atm f_th1 f_th2)
     | step ctxt isFO thpairs (_, Metis.Proof.Refl f_tm)                           =
         refl_inf ctxt f_tm
     | step ctxt isFO thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
         equality_inf ctxt isFO thpairs f_lit f_p f_r;
-
-  val factor = Seq.hd o distinct_subgoals_tac;
 
   fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
 
   fun translate isFO _    thpairs [] = thpairs
     | translate isFO ctxt thpairs ((fol_th, inf) :: infpairs) =
         let val _ = Output.debug (fn () => "=============================================")
             val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
             val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
-            val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf)))
+            val th = Meson.flexflex_first_order (step ctxt isFO thpairs (fol_th, inf))
             val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm th)
             val _ = Output.debug (fn () => "=============================================")
             val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
         in
             if nprems_of th = n_metis_lits then ()