src/HOL/Tools/datatype_realizer.ML

           (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
     val cert = cterm_of sg;
     val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
       (HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
 
-    val thm = simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
+    val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
       (fn prems =>
          [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
           rtac (cterm_instantiate inst induction) 1,
           ALLGOALS ObjectLogic.atomize_tac,
           rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),

     val r = Const (case_name, map fastype_of rs ---> T --> rT);
 
     val y = Var (("y", 0), Type.varifyT T);
     val y' = Free ("y", T);
 
-    val thm = prove_goalw_cterm [] (cert (Logic.list_implies (prems,
+    val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
       HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
         list_comb (r, rs @ [y'])))))
       (fn prems =>
          [rtac (cterm_instantiate [(cert y, cert y')] exhaustion) 1,
           ALLGOALS (EVERY'