src/HOL/Tools/metis_tools.ML

             val args   = map hol_term_to_fol_FO tms
         in Metis.Term.Fn (c, tyargs @ args) end
     | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v
     | _ => error "hol_term_to_fol_FO";
 
-fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a
-  | hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) =
-      Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist)
-  | hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) =
-       Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]);
+fun hol_term_to_fol_HO (ResHolClause.CombVar (a, _)) = Metis.Term.Var a
+  | hol_term_to_fol_HO (ResHolClause.CombConst (a, _, tylist)) =
+      Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
+  | hol_term_to_fol_HO (ResHolClause.CombApp (tm1, tm2)) =
+       Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
 
 (*The fully-typed translation, to avoid type errors*)
 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
 
 fun hol_term_to_fol_FT (ResHolClause.CombVar(a, ty)) =

 
 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
 fun metis_of_typeLit pos (ResClause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
   | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
 
-fun default_sort ctxt (TVar _) = false
-  | default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
+fun default_sort _ (TVar _) = false
+  | default_sort ctxt (TFree (x, s)) = (s = Option.getOpt (Variable.def_sort ctxt (x, ~1), []));
 
 fun metis_of_tfree tf =
   Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
 
 fun hol_thm_to_fol is_conjecture ctxt mode th =

 (* CLASSREL CLAUSE *)
 
 fun m_classrel_cls subclass superclass =
   [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
 
-fun classrel_cls (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) =
+fun classrel_cls (ResClause.ClassrelClause {subclass, superclass, ...}) =
   (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
 
 (* ------------------------------------------------------------------------- *)
 (* FOL to HOL  (Metis to Isabelle)                                           *)
 (* ------------------------------------------------------------------------- *)

 fun terms_of [] = []
   | terms_of (Term t :: tts) = t :: terms_of tts
   | terms_of (Type _ :: tts) = terms_of tts;
 
 fun types_of [] = []
-  | types_of (Term (Term.Var((a,idx), T)) :: tts) =
+  | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
       if String.isPrefix "_" a then
           (*Variable generated by Metis, which might have been a type variable.*)
-          TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts
+          TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
       else types_of tts
   | types_of (Term _ :: tts) = types_of tts
   | types_of (Type T :: tts) = T :: types_of tts;
 
 fun apply_list rator nargs rands =

 
 (*Remove the "apply" operator from an HO term*)
 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   | strip_happ args x = (x, args);
 
-fun fol_type_to_isa ctxt (Metis.Term.Var v) =
+fun fol_type_to_isa _ (Metis.Term.Var v) =
      (case Recon.strip_prefix ResClause.tvar_prefix v of
           SOME w => Recon.make_tvar w
         | NONE   => Recon.make_tvar v)
   | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
      (case Recon.strip_prefix ResClause.tconst_prefix x of

   in  case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected"  end;
 
 (*Maps fully-typed metis terms to isabelle terms*)
 fun fol_term_to_hol_FT ctxt fol_tm =
   let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
-      fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, ty])) =
+      fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
              (case Recon.strip_prefix ResClause.schematic_var_prefix v of
                   SOME w =>  mk_var(w, dummyT)
                 | NONE   => mk_var(v, dummyT))
-        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), ty])) =
+        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
             Const ("op =", HOLogic.typeT)
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
            (case Recon.strip_prefix ResClause.const_prefix x of
                 SOME c => Const (Recon.invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)

       val [vx] = Term.add_vars (prop_of th) []
       val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
   in  cterm_instantiate substs th  end;
 
 (* INFERENCE RULE: AXIOM *)
-fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th);
+fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th);
     (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
 
 (* INFERENCE RULE: ASSUME *)
 fun assume_inf ctxt mode atm =
   inst_excluded_middle

       | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
   end;
 
 fun resolve_inf ctxt mode thpairs atm th1 th2 =
   let
-    val thy = ProofContext.theory_of ctxt
     val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
     val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
     val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   in
     if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)

       val i_t = singleton (fol_terms_to_hol ctxt mode) t
       val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
       val c_t = cterm_incr_types thy refl_idx i_t
   in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
 
-fun get_ty_arg_size thy (Const("op =",_)) = 0  (*equality has no type arguments*)
-  | get_ty_arg_size thy (Const(c,_))      = (Recon.num_typargs thy c handle TYPE _ => 0)
-  | get_ty_arg_size thy _      = 0;
+fun get_ty_arg_size _ (Const ("op =", _)) = 0  (*equality has no type arguments*)
+  | get_ty_arg_size thy (Const (c, _)) = (Recon.num_typargs thy c handle TYPE _ => 0)
+  | get_ty_arg_size _ _ = 0;
 
 (* INFERENCE RULE: EQUALITY *)
-fun equality_inf ctxt mode thpairs (pos,atm) fp fr =
+fun equality_inf ctxt mode (pos, atm) fp fr =
   let val thy = ProofContext.theory_of ctxt
       val m_tm = Metis.Term.Fn atm
       val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
       val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
-      fun replace_item_list lx 0 (l::ls) = lx::ls
+      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_FO tm [] = (tm, Term.Bound 0)
         | path_finder_FO tm (p::ps) =
             let val (tm1,args) = Term.strip_comb tm
                 val adjustment = get_ty_arg_size thy tm1

             in
                 (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) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
+        | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
       fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
-        | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1,t2])) =
+        | 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,t2])) =
+        | 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 (".", [t1,t2])) =
+        | 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)
       fun path_finder FO tm ps _ = path_finder_FO tm ps
         | path_finder HO (tm as Const("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*)
-        | path_finder HO tm (p::ps) (Metis.Term.Fn ("{}", [t1])) =
+        | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
              path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
         | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps)
                             (Metis.Term.Fn ("=", [t1,t2])) =
              (*equality: not curried, as other predicates are*)
              if p=0 then path_finder_FT tm (0::1::ps)
                           (Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2]))
                           (*select first operand*)
              else path_finder_FT tm (p::ps)
                    (Metis.Term.Fn (".", [metis_eq,t2]))
                    (*1 selects second operand*)
-        | path_finder FT tm (p::ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
+        | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
              (*if not equality, ignore head to skip the hBOOL predicate*)
         | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
       fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
             let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
             in (tm, nt $ tm_rslt) end

                          (ListPair.zip (OldTerm.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 mode thpairs (fol_th, Metis.Proof.Axiom _)                        =
-      factor (axiom_inf ctxt thpairs fol_th)
-  | step ctxt mode thpairs (_, Metis.Proof.Assume f_atm)                        =
-      assume_inf ctxt mode f_atm
-  | step ctxt mode thpairs (_, Metis.Proof.Subst(f_subst, f_th1))               =
+fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th)
+  | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm
+  | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) =
       factor (inst_inf ctxt mode thpairs f_subst f_th1)
-  | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2))        =
+  | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
       factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
-  | step ctxt mode thpairs (_, Metis.Proof.Refl f_tm)                           =
-      refl_inf ctxt mode f_tm
-  | step ctxt mode thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
-      equality_inf ctxt mode thpairs f_lit f_p f_r;
-
-fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
-
-fun translate mode _    thpairs [] = thpairs
+  | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm
+  | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
+      equality_inf ctxt mode f_lit f_p f_r;
+
+fun real_literal (_, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
+
+fun translate _ _ thpairs [] = thpairs
   | translate mode ctxt 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)
           val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
           val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
           val _ = trace_msg (fn () => "=============================================")
-          val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
+          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 ()
           else error "Metis: proof reconstruction has gone wrong";
           translate mode ctxt ((fol_th, th) :: thpairs) infpairs
       end;
 
 (*Determining which axiom clauses are actually used*)
 fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
-  | used_axioms axioms _                         = NONE;
+  | used_axioms _ _ = NONE;
 
 (* ------------------------------------------------------------------------- *)
 (* Translation of HO Clauses                                                 *)
 (* ------------------------------------------------------------------------- *)
 

 
 fun type_ext thy tms =
   let val subs = ResAtp.tfree_classes_of_terms tms
       val supers = ResAtp.tvar_classes_of_terms tms
       and tycons = ResAtp.type_consts_of_terms thy tms
-      val arity_clauses = ResClause.make_arity_clauses thy tycons supers
-      val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
+      val (supers', arity_clauses) = ResClause.make_arity_clauses thy tycons supers
       val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
   end;
 
 (* ------------------------------------------------------------------------- *)

 
 type logic_map =
   {axioms : (Metis.Thm.thm * Thm.thm) list,
    tfrees : ResClause.type_literal list};
 
-fun const_in_metis c (pol,(pred,tm_list)) =
+fun const_in_metis c (pred, tm_list) =
   let
-    fun in_mterm (Metis.Term.Var nm) = false
+    fun in_mterm (Metis.Term.Var _) = false
       | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
       | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
-  in  c=pred orelse exists in_mterm tm_list  end;
+  in  c = pred orelse exists in_mterm tm_list  end;
 
 (*Extract TFree constraints from context to include as conjecture clauses*)
 fun init_tfrees ctxt =
   let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
   in  ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;

         end;
       val lmap0 = List.foldl (add_thm true)
                         {axioms = [], tfrees = init_tfrees ctxt} cls
       val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths
       val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
-      fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
+      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 [comb_I] else []
       val thK  = if used "c_COMBK" then [comb_K] else []
       val thB   = if used "c_COMBB" then [comb_B] else []
       val thC   = if used "c_COMBC" then [comb_C] else []

                 val proof = Metis.Proof.proof mth
                 val result = translate mode ctxt' axioms proof
                 and used = map_filter (used_axioms axioms) proof
                 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
                 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
-                val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
+                val unused = filter (fn (_, cls) => not (common_thm used cls)) th_cls_pairs
             in
                 if null unused then ()
                 else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
                 case result of
                     (_,ith)::_ =>