src/HOL/Library/Old_SMT/old_smt_normalize.ML

   val (cpfalse, cfalse) =
     `Old_SMT_Utils.mk_cprop (Thm.cterm_of @{context} @{const False})
 
   fun inst f ct thm =
     let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
-    in Thm.instantiate ([], [(cv, ct)]) thm end
+    in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end
 in
 
 fun instantiate_elim thm =
   (case Thm.concl_of thm of
     @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm

     mk_meta_eq @{lemma "p = trigger t p" by (simp add: trigger_def)}
 
   fun insert_trigger_conv [] ct = Conv.all_conv ct
     | insert_trigger_conv ctss ct =
         let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
-        in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end
+        in Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]) trigger_eq end
 
   fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
     let
       val (lhs, rhs) = dest_cond_eq ct
 

   val weight_eq =
     mk_meta_eq @{lemma "p = weight i p" by (simp add: weight_def)}
   fun mk_weight_eq w =
     let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq)
     in
-      Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq
+      Thm.instantiate ([], [(dest_Var (Thm.term_of cv), Numeral.mk_cnumber @{ctyp int} w)])
+        weight_eq
     end
 
   fun add_weight_conv NONE _ = Conv.all_conv
     | add_weight_conv (SOME weight) ctxt =
         let val cv = Conv.rewr_conv (mk_weight_eq weight)