src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML

     Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
   end;
 
 fun cterm_instantiate_pos cts thm =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_thm thm);
+    val thy = Thm.theory_of_thm thm;
     val vars = Term.add_vars (Thm.prop_of thm) [];
     val vars' = rev (drop (length vars - length cts) vars);
-    val ps = map_filter (fn (_, NONE) => NONE
-      | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
+    val ps =
+      map_filter
+        (fn (_, NONE) => NONE
+          | (var, SOME ct) => SOME (Thm.cterm_of thy (Var var), ct)) (vars' ~~ cts);
   in
     Drule.cterm_instantiate ps thm
   end;
 
 fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);