src/HOL/Integ/int_arith1.ML

   struct
   fun prove_conv tacs sg (hyps: thm list) xs (t, u) =
     if t aconv u then NONE
     else
       let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
-      in SOME (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
+      in SOME (Goal.prove sg xs [] eq (K (EVERY tacs))) end
 
   fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
   fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
 
   fun prep_simproc (name, pats, proc) =