src/Pure/Isar/element.ML

 
 fun standard_elim th =
   (case Object_Logic.elim_concl th of
     SOME C =>
       let
-        val cert = Thm.cterm_of (Thm.theory_of_thm th);
+        val thy = Thm.theory_of_thm th;
         val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
-        val th' = Thm.instantiate ([], [(cert C, cert thesis)]) th;
+        val th' = Thm.instantiate ([], [(Thm.cterm_of thy C, Thm.cterm_of thy thesis)]) th;
       in (th', true) end
   | NONE => (th, false));
 
 fun thm_name kind th prts =
   let val head =

 
 (* derived rules *)
 
 fun instantiate_tfrees thy subst th =
   let
-    val certT = Thm.ctyp_of thy;
     val idx = Thm.maxidx_of th + 1;
-    fun cert_inst (a, (S, T)) = (certT (TVar ((a, idx), S)), certT T);
+    fun cert_inst (a, (S, T)) = (Thm.ctyp_of thy (TVar ((a, idx), S)), Thm.ctyp_of thy T);
 
     fun add_inst (a, S) insts =
       if AList.defined (op =) insts a then insts
       else (case AList.lookup (op =) subst a of NONE => insts | SOME T => (a, (S, T)) :: insts);
     val insts =

     |> Thm.generalize (map fst insts, []) idx
     |> Thm.instantiate (map cert_inst insts, [])
   end;
 
 fun instantiate_frees thy subst =
-  let val cert = Thm.cterm_of thy in
-    Drule.forall_intr_list (map (cert o Free o fst) subst) #>
-    Drule.forall_elim_list (map (cert o snd) subst)
-  end;
+  Drule.forall_intr_list (map (Thm.cterm_of thy o Free o fst) subst) #>
+  Drule.forall_elim_list (map (Thm.cterm_of thy o snd) subst);
 
 fun hyps_rule rule th =
   let val {hyps, ...} = Thm.crep_thm th in
     Drule.implies_elim_list
       (rule (Drule.implies_intr_list hyps th))