1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
     1.3 @@ -15,7 +15,6 @@
     1.4      Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
     1.5      -> term
     1.6    val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
     1.7 -  val metis_aconv_untyped : term * term -> bool
     1.8    val replay_one_inference :
     1.9      Proof.context -> (string * term) list -> int Symtab.table
    1.10      -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
    1.11 @@ -209,18 +208,6 @@
    1.12    | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
    1.13    | simp_not_not t = t
    1.14  
    1.15 -(* Match untyped terms. *)
    1.16 -fun metis_aconv_untyped (Const (a, _), Const(b, _)) = (a = b)
    1.17 -  | metis_aconv_untyped (Free (a, _), Free (b, _)) = (a = b)
    1.18 -  | metis_aconv_untyped (Var ((a, _), _), Var ((b, _), _)) =
    1.19 -    a = b (* ignore variable numbers *)
    1.20 -  | metis_aconv_untyped (Bound i, Bound j) = (i = j)
    1.21 -  | metis_aconv_untyped (Abs (_, _, t), Abs (_, _, u)) =
    1.22 -    metis_aconv_untyped (t, u)
    1.23 -  | metis_aconv_untyped (t1 $ t2, u1 $ u2) =
    1.24 -    metis_aconv_untyped (t1, u1) andalso metis_aconv_untyped (t2, u2)
    1.25 -  | metis_aconv_untyped _ = false
    1.26 -
    1.27  val normalize_literal = simp_not_not o Envir.eta_contract
    1.28  
    1.29  (* Find the relative location of an untyped term within a list of terms as a
    1.30 @@ -229,7 +216,7 @@
    1.31    let
    1.32      fun match_lit normalize =
    1.33        HOLogic.dest_Trueprop #> normalize
    1.34 -      #> curry metis_aconv_untyped (lit |> normalize)
    1.35 +      #> curry Term.aconv_untyped (lit |> normalize)
    1.36    in
    1.37      (case find_index (match_lit I) haystack of
    1.38         ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
    1.39 @@ -434,7 +421,7 @@
    1.40        let
    1.41          val (prems0, concl) = th |> prop_of |> Logic.strip_horn
    1.42          val prems = prems0 |> map normalize_literal
    1.43 -                           |> distinct metis_aconv_untyped
    1.44 +                           |> distinct Term.aconv_untyped
    1.45          val goal = Logic.list_implies (prems, concl)
    1.46          val tac = cut_rules_tac [th] 1
    1.47                    THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
    1.48 @@ -484,7 +471,7 @@
    1.49      val prem = goal |> Logic.strip_assums_hyp |> hd
    1.50      val concl = goal |> Logic.strip_assums_concl
    1.51      fun pair_untyped_aconv (t1, t2) (u1, u2) =
    1.52 -      metis_aconv_untyped (t1, u1) andalso metis_aconv_untyped (t2, u2)
    1.53 +      Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2)
    1.54      fun add_terms tp inst =
    1.55        if exists (pair_untyped_aconv tp) inst then inst
    1.56        else tp :: map (apsnd (subst_atomic [tp])) inst

     2.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Jun 09 00:16:28 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Jun 09 00:16:28 2011 +0200
     2.3 @@ -56,7 +56,7 @@
     2.4  
     2.5  (* Designed to work also with monomorphic instances of polymorphic theorems. *)
     2.6  fun have_common_thm ths1 ths2 =
     2.7 -  exists (member (metis_aconv_untyped o pairself prop_of) ths1)
     2.8 +  exists (member (Term.aconv_untyped o pairself prop_of) ths1)
     2.9           (map Meson.make_meta_clause ths2)
    2.10  
    2.11  (*Determining which axiom clauses are actually used*)