src/Pure/drule.ML

   val eta_contraction_rule: thm -> thm
   val norm_hhf_eq: thm
   val is_norm_hhf: term -> bool
   val norm_hhf: theory -> term -> term
   val norm_hhf_cterm: cterm -> cterm
-  val unvarify: thm -> thm
   val protect: cterm -> cterm
   val protectI: thm
   val protectD: thm
   val protect_cong: thm
   val implies_intr_protected: cterm list -> thm -> thm

 
 (*maps A1,...,An |- B  to  [| A1;...;An |] ==> B*)
 val implies_intr_list = fold_rev implies_intr;
 
 (*maps [| A1;...;An |] ==> B and [A1,...,An]  to  B*)
-fun implies_elim_list impth ths = Library.foldl (uncurry implies_elim) (impth,ths);
+fun implies_elim_list impth ths = fold Thm.elim_implies ths impth;
 
 (*Reset Var indexes to zero, renaming to preserve distinctness*)
 fun zero_var_indexes_list [] = []
   | zero_var_indexes_list ths =
       let

            raise THM("cterm_instantiate: incompatible theories",0,[th])
        | TYPE (msg, _, _) => raise THM(msg, 0, [th])
 end;
 
 
-(* global schematic variables *)
-
-fun unvarify th =
-  let
-    val thy = Thm.theory_of_thm th;
-    val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
-
-    val prop = Thm.full_prop_of th;
-    val _ = map Logic.unvarify (prop :: Thm.hyps_of th)
-      handle TERM (msg, _) => raise THM (msg, 0, [th]);
-
-    val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
-    val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
-    val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
-      let val T' = TermSubst.instantiateT instT0 T
-      in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
-  in Thm.instantiate (instT, inst) th end;
-
-
 (** protected propositions and embedded terms **)
 
 local
   val A = cert (Free ("A", propT));
-  val prop_def = unvarify ProtoPure.prop_def;
-  val term_def = unvarify ProtoPure.term_def;
+  val prop_def = Thm.unvarify ProtoPure.prop_def;
+  val term_def = Thm.unvarify ProtoPure.term_def;
 in
   val protect = Thm.capply (cert Logic.protectC);
   val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
       (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
   val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard