diff -r 854f667df3d6 -r 8d7fc4a5b502 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
@@ -15,7 +15,6 @@
     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
@@ -209,18 +208,6 @@
   | 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
@@ -229,7 +216,7 @@
   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
@@ -434,7 +421,7 @@
       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]}
@@ -484,7 +471,7 @@
     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