src/HOL/Tools/Metis/metis_reconstruct.ML

 
   val hol_clause_from_metis :
     Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
     -> term
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
-  val metis_aconv_untyped : term * term -> bool
   val replay_one_inference :
     Proof.context -> (string * term) list -> int Symtab.table
     -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
     -> (Metis_Thm.thm * thm) list
   val discharge_skolem_premises :

   | s_not t = HOLogic.mk_not t
 fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
   | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
   | simp_not_not t = t
 
-(* Match untyped terms. *)
-fun metis_aconv_untyped (Const (a, _), Const(b, _)) = (a = b)
-  | metis_aconv_untyped (Free (a, _), Free (b, _)) = (a = b)
-  | metis_aconv_untyped (Var ((a, _), _), Var ((b, _), _)) =
-    a = b (* ignore variable numbers *)
-  | metis_aconv_untyped (Bound i, Bound j) = (i = j)
-  | metis_aconv_untyped (Abs (_, _, t), Abs (_, _, u)) =
-    metis_aconv_untyped (t, u)
-  | metis_aconv_untyped (t1 $ t2, u1 $ u2) =
-    metis_aconv_untyped (t1, u1) andalso metis_aconv_untyped (t2, u2)
-  | metis_aconv_untyped _ = false
-
 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. *)
 fun index_of_literal lit haystack =
   let
     fun match_lit normalize =
       HOLogic.dest_Trueprop #> normalize
-      #> curry metis_aconv_untyped (lit |> normalize)
+      #> curry Term.aconv_untyped (lit |> normalize)
   in
     (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

       th
     else
       let
         val (prems0, concl) = th |> prop_of |> Logic.strip_horn
         val prems = prems0 |> map normalize_literal
-                           |> distinct metis_aconv_untyped
+                           |> distinct Term.aconv_untyped
         val goal = Logic.list_implies (prems, concl)
         val tac = cut_rules_tac [th] 1
                   THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
                   THEN ALLGOALS assume_tac
       in

   let
     val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
     val prem = goal |> Logic.strip_assums_hyp |> hd
     val concl = goal |> Logic.strip_assums_concl
     fun pair_untyped_aconv (t1, t2) (u1, u2) =
-      metis_aconv_untyped (t1, u1) andalso metis_aconv_untyped (t2, u2)
+      Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2)
     fun add_terms tp inst =
       if exists (pair_untyped_aconv tp) inst then inst
       else tp :: map (apsnd (subst_atomic [tp])) inst
     fun is_flex t =
       case strip_comb t of