src/HOL/Rat.thy

     (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
   #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2]
     (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
   #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
       @{thm True_implies_equals},
-      read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
-      read_instantiate @{context} [(("a", 0), "(- numeral ?v)")] @{thm distrib_left},
+      @{thm distrib_left [where a = "numeral v" for v]},
+      @{thm distrib_left [where a = "- numeral v" for v]},
       @{thm divide_1}, @{thm divide_zero_left},
       @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
       @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
       @{thm of_int_minus}, @{thm of_int_diff},
       @{thm of_int_of_nat_eq}]