src/HOL/Algebra/abstract/Ring.thy

         ["t + u::'a::ring",
 	 "t - u::'a::ring",
 	 "t * u::'a::ring",
 	 "- t::'a::ring"];
     fun proc sg ss t = 
-      let val rew = Tactic.prove sg [] []
+      let val rew = Goal.prove sg [] []
             (HOLogic.mk_Trueprop
               (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
                 (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
             |> mk_meta_eq;
           val (t', u) = Logic.dest_equals (Thm.prop_of rew);