# HG changeset patch
# User blanchet
# Date 1286379777 -7200
# Node ID 415556559fada985515b22b23cbaa657334f394f
# Parent  03174b2d075c09ef95582cd7863d50e43893dbff
get rid of function that duplicates existing Pure functionality

diff -r 03174b2d075c -r 415556559fad src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Wed Oct 06 17:38:06 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Wed Oct 06 17:42:57 2010 +0200
@@ -59,23 +59,7 @@
 
 (* FIXME ### GET RID OF skolem WRAPPER by looking at substitution *)
 
-(* FIXME ### try cterm_instantiate *)
-fun instantiate_theorem thy inst th =
-  let
-    val tyenv = Vartab.empty |> fold (Type.raw_unify o pairself fastype_of) inst
-    val instT =
-      [] |> Vartab.fold (fn (z, (S, T)) =>
-                            cons (TVar (z, S), Type.devar tyenv T)) tyenv
-    val inst = inst |> map (pairself (subst_atomic_types instT))
-    val _ = trace_msg (fn () => cat_lines (map (fn (T, U) =>
-        Syntax.string_of_typ @{context} T ^ " |-> " ^
-        Syntax.string_of_typ @{context} U) instT))
-    val _ = trace_msg (fn () => cat_lines (map (fn (t, u) =>
-        Syntax.string_of_term @{context} t ^ " |-> " ^
-        Syntax.string_of_term @{context} u) inst))
-    val cinstT = instT |> map (pairself (ctyp_of thy))
-    val cinst = inst |> map (pairself (cterm_of thy))
-  in th |> Thm.instantiate (cinstT, cinst) end
+fun term_instantiate thy = cterm_instantiate o map (pairself (cterm_of thy))
 
 (* In principle, it should be sufficient to apply "assume_tac" to unify the
    conclusion with one of the premises. However, in practice, this is unreliable
@@ -119,7 +103,7 @@
       | (Var _, _) => add_terms (t, u)
       | (_, Var _) => add_terms (u, t)
       | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
-  in th |> instantiate_theorem thy (unify_terms (prem, concl) []) end
+  in th |> term_instantiate thy (unify_terms (prem, concl) []) end
 
 fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no)
 fun shuffle_ord p =
@@ -145,7 +129,7 @@
     val t' = t |> repair |> fold (curry absdummy) (map snd params)
     fun do_instantiate th =
       let val var = Term.add_vars (prop_of th) [] |> the_single in
-        th |> instantiate_theorem thy [(Var var, t')]
+        th |> term_instantiate thy [(Var var, t')]
       end
   in
     etac @{thm allE} i