src/HOL/Tools/Sledgehammer/metis_tactics.ML

       (CombConst ((c, _), _, tys), tms) =>
         let val tyargs = map hol_type_to_fol tys
             val args   = map hol_term_to_fol_FO tms
         in Metis.Term.Fn (c, tyargs @ args) end
     | (CombVar ((v, _), _), []) => Metis.Term.Var v
-    | _ => error "hol_term_to_fol_FO";
+    | _ => raise Fail "hol_term_to_fol_FO";
 
 fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
   | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
       Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
   | hol_term_to_fol_HO (CombApp (tm1, tm2)) =

   | types_of (Type T :: tts) = T :: types_of tts;
 
 fun apply_list rator nargs rands =
   let val trands = terms_of rands
   in  if length trands = nargs then Term (list_comb(rator, trands))
-      else error
+      else raise Fail
         ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
           " expected " ^ Int.toString nargs ^
           " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
   end;
 

      (case strip_prefix tconst_prefix x of
           SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
         | NONE    =>
       case strip_prefix tfree_prefix x of
           SOME tf => mk_tfree ctxt tf
-        | NONE    => error ("fol_type_to_isa: " ^ x));
+        | NONE    => raise Fail ("fol_type_to_isa: " ^ x));
 
 fun reintroduce_skolem_Eps thy skolem_somes =
   let
     fun aux Ts args t =
       case t of

             let val (rator,rands) = strip_happ [] t
             in  case rator of
                     Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
                   | _ => case tm_to_tt rator of
                              Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
-                           | _ => error "tm_to_tt: HO application"
+                           | _ => raise Fail "tm_to_tt: HO application"
             end
         | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
       and applic_to_tt ("=",ts) =
             Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
         | applic_to_tt (a,ts) =

                       val nterms = length ts - ntypes
                       val tts = map tm_to_tt ts
                       val tys = types_of (List.take(tts,ntypes))
                   in if length tys = ntypes then
                          apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
-                     else error ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
-                                 " but gets " ^ Int.toString (length tys) ^
-                                 " type arguments\n" ^
-                                 cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
-                                 " the terms are \n" ^
-                                 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
+                     else
+                       raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
+                                   " but gets " ^ Int.toString (length tys) ^
+                                   " type arguments\n" ^
+                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
+                                   " the terms are \n" ^
+                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
                      end
               | NONE => (*Not a constant. Is it a type constructor?*)
             case strip_prefix tconst_prefix a of
                 SOME b =>
                   Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))

               | NONE => (*a fixed variable? They are Skolem functions.*)
             case strip_prefix fixed_var_prefix a of
                 SOME b =>
                   let val opr = Term.Free(b, HOLogic.typeT)
                   in  apply_list opr (length ts) (map tm_to_tt ts)  end
-              | NONE => error ("unexpected metis function: " ^ a)
+              | NONE => raise Fail ("unexpected metis function: " ^ a)
   in
     case tm_to_tt fol_tm of
       Term t => t
-    | _ => error "fol_tm_to_tt: Term expected"
+    | _ => raise Fail "fol_tm_to_tt: Term expected"
   end
 
 (*Maps fully-typed metis terms to isabelle terms*)
 fun hol_term_from_fol_FT ctxt fol_tm =
   let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^

            (case strip_prefix const_prefix x of
                 SOME c => Const (invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix fixed_var_prefix x of
                 SOME v => Free (v, fol_type_to_isa ctxt ty)
-              | NONE => error ("hol_term_from_fol_FT bad constant: " ^ x))
+              | NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x))
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
             cvt tm1 $ cvt tm2
         | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
             cvt tm1 $ cvt tm2
         | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)

    trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
    trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
 
 fun lookth thpairs (fth : Metis.Thm.thm) =
   the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
-  handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
+  handle Option =>
+         raise Fail ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
 
 fun is_TrueI th = Thm.eq_thm(TrueI,th);
 
 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
 

                               (Metis.Term.Fn atm)
         val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
         val prems_th1 = prems_of i_th1
         val prems_th2 = prems_of i_th2
         val index_th1 = get_index (mk_not i_atm) prems_th1
-              handle Empty => error "Failed to find literal in th1"
+              handle Empty => raise Fail "Failed to find literal in th1"
         val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
         val index_th2 = get_index i_atm prems_th2
-              handle Empty => error "Failed to find literal in th2"
+              handle Empty => raise Fail "Failed to find literal in th2"
         val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
     in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
   end;
 
 (* INFERENCE RULE: REFL *)

                 (r, list_comb (tm1, replace_item_list t p' args))
             end
       fun path_finder_HO tm [] = (tm, Term.Bound 0)
         | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
         | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
+        | path_finder_HO tm ps =
+          raise Fail ("equality_inf, path_finder_HO: path = " ^
+                      space_implode " " (map Int.toString ps) ^
+                      " isa-term: " ^  Syntax.string_of_term ctxt tm)
       fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
         | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) =
             path_finder_FT tm ps t1
         | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) =
             (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
         | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) =
             (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
-        | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^
-                                        space_implode " " (map Int.toString ps) ^
-                                        " isa-term: " ^  Syntax.string_of_term ctxt tm ^
-                                        " fol-term: " ^ Metis.Term.toString t)
+        | path_finder_FT tm ps t =
+          raise Fail ("equality_inf, path_finder_FT: path = " ^
+                      space_implode " " (map Int.toString ps) ^
+                      " isa-term: " ^  Syntax.string_of_term ctxt tm ^
+                      " fol-term: " ^ Metis.Term.toString t)
       fun path_finder FO tm ps _ = path_finder_FO tm ps
         | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
              (*equality: not curried, as other predicates are*)
              if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
              else path_finder_HO tm (p::ps)        (*1 selects second operand*)

   | (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =>
     equality_inf ctxt mode skolem_somes f_lit f_p f_r
 
 fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
 
-(* TODO: use "fold" instead *)
+(* FIXME: use "fold" instead *)
 fun translate _ _ _ thpairs [] = thpairs
   | translate ctxt mode skolem_somes thpairs ((fol_th, inf) :: infpairs) =
       let val _ = trace_msg (fn () => "=============================================")
           val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
           val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)

         in
            {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
             tfrees = union (op =) tfree_lits tfrees,
             skolem_somes = skolem_somes}
         end;
-      val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
-                 |> fold (add_thm true) cls
-                 |> add_tfrees
-                 |> fold (add_thm false) ths
+      val lmap as {skolem_somes, ...} =
+        {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
+        |> fold (add_thm true) cls
+        |> add_tfrees
+        |> fold (add_thm false) ths
       val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
       fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
       (*Now check for the existence of certain combinators*)
       val thI  = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else []
       val thK  = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else []

       val thEQ  = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
       val lmap =
         lmap |> mode <> FO
                 ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI)
   in
-      (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap)
+      (mode, add_type_thm (type_ext thy 
+                                (* FIXME: Call"kill_skolem_Eps" here? *)
+                          (map ((*snd o kill_skolem_Eps ~1 skolem_somes o*) prop_of)
+                               (cls @ ths))) lmap)
   end;
 
 fun refute cls =
     Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);