src/HOL/Tools/Metis/metis_reconstruct.ML

 
 signature METIS_RECONSTRUCT =
 sig
   type type_enc = ATP_Problem_Generate.type_enc
 
-  exception METIS of string * string
+  exception METIS_RECONSTRUCT of string * string
 
   val hol_clause_from_metis :
     Proof.context -> type_enc -> int Symtab.table
     -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a

 open ATP_Problem
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 open Metis_Generate
 
-exception METIS of string * string
+exception METIS_RECONSTRUCT of string * string
 
 fun atp_name_from_metis type_enc s =
   case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
     SOME ((s, _), (_, swap)) => (s, swap)
   | _ => (s, false)

         cat_lines ("subst_translations:" ::
           (substs' |> map (fn (x, y) =>
             Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
             Syntax.string_of_term ctxt (term_of y)))));
   in cterm_instantiate substs' i_th end
-  handle THM (msg, _, _) => raise METIS ("inst_inference", msg)
-       | ERROR msg => raise METIS ("inst_inference", msg)
+  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 inc th =

              (trace_msg ctxt (fn () => "Failed to find literal in \"th2\"");
               i_th2)
            | j2 =>
              (trace_msg ctxt (fn () => "  index th2: " ^ string_of_int j2);
               resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2
-              handle TERM (s, _) => raise METIS ("resolve_inference", s)))
+              handle TERM (s, _) =>
+                     raise METIS_RECONSTRUCT ("resolve_inference", s)))
       end
   end
 
 (* INFERENCE RULE: REFL *)
 

         hol_terms_from_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 ("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 => ""))
+        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

         val tac = cut_tac th 1
                   THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
                   THEN ALLGOALS assume_tac
       in
         if length prems = length prems0 then
-          raise METIS ("resynchronize", "Out of sync")
+          raise METIS_RECONSTRUCT ("resynchronize", "Out of sync")
         else
           Goal.prove ctxt [] [] goal (K tac)
           |> resynchronize ctxt fol_th
       end
   end