src/HOL/List.thy

         val Type(_,listT::_) = eqT
         val appT = [listT,listT] ---> listT
         val app = Const("List.op @",appT)
         val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
-        val thm = Tactic.prove sg [] [] eq
+        val thm = Goal.prove sg [] [] eq
           (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
       in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
 
   in
     if list1 lastl andalso list1 lastr then rearr append1_eq_conv